1 /-
2 Copyright (c) 2015, 2017 Jeremy Avigad. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Jeremy Avigad, Robert Y. Lewis, Johannes Hölzl, Mario Carneiro, Sébastien Gouëzel
5 -/
6
7 import data.real.nnreal data.real.ennreal
src └──────────────┘ └───────────────┘
8 import topology.uniform_space.separation topology.uniform_space.uniform_embedding topology.uniform_space.pi
src └───────────────────────────────┘ └──────────────────────────────────────┘ └───────────────────────┘
9 import topology.bases
src └────────────┘
10
11 /-!
12 # Extended metric spaces
13
14 This file is devoted to the definition and study of `emetric_spaces`, i.e., metric
15 spaces in which the distance is allowed to take the value ∞. This extended distance is
16 called `edist`, and takes values in `ennreal`.
17
18 Many definitions and theorems expected on emetric spaces are already introduced on uniform spaces and
19 topological spaces. For example:
20 open and closed sets, compactness, completeness, continuity and uniform continuity
21
22 The class `emetric_space` therefore extends `uniform_space` (and `topological_space`).
23 -/
24
25 open lattice set filter classical
26 noncomputable theory
27
28 open_locale uniformity topological_space
29
30 universes u v w
31 variables {α : Type u} {β : Type v} {γ : Type w}
32
33 /-- Characterizing uniformities associated to a (generalized) distance function `D`
34 in terms of the elements of the uniformity. -/
35 theorem uniformity_dist_of_mem_uniformity [linear_order β] {U : filter (α × α)} (z : β) (D : α → α → β)
id └──────────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────┘ └────┘ ┴
typ └──────────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
36 (H : ∀ s, s ∈ U ↔ ∃ε>z, ∀{a b:α}, D a b < ε → (a, b) ∈ s) :
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
37 U = ⨅ ε>z, principal {p:α×α | D p.1 p.2 < ε} :=
id ┴ ┴ ┴ ┴ ┴┴ └───────┘ ┴ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ └───────┘ ┴ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴
doc ┴ ┴ └───────┘
38 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
39 (le_infi $ λ ε, le_infi $ λ ε0, le_principal_iff.2 $ (H _).2 ⟨ε, ε0, λ a b, id⟩)
id └─────┘ ┴ └─────┘ └┘ └──────────────┘┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
src └─────┘ └─────┘ └──────────────┘┴ ┴ └┘
typ └─────┘ ┴ └─────┘ └┘ └──────────────┘┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
40 (λ r ur, let ⟨ε, ε0, h⟩ := (H _).1 ur in
id ┴ └┘ └─┘ ┴ └┘ ┴ ┴ ┴ └┘
src ┴
typ ┴ └┘ └─┘ ┴ └┘ ┴ ┴ ┴ └┘
41 mem_infi_sets ε $ mem_infi_sets ε0 $ mem_principal_sets.2 $ λ ⟨a, b⟩, h)
id └───────────┘ └───────────┘ └────────────────┘┴ ┴
src └───────────┘ └───────────┘ └────────────────┘┴
typ └───────────┘ └───────────┘ └────────────────┘┴ ┴
42
43 class has_edist (α : Type*) := (edist : α → α → ennreal)
id └───┘ ┴ ┴ ┴ └─────┘
src └─────┘
typ └───┘ ┴ ┴ ┴ └─────┘
doc └─────┘
44 export has_edist (edist)
45
46 /- Design note: one could define an `emetric_space` just by giving `edist`, and then
47 derive an instance of `uniform_space` by taking the natural uniform structure
48 associated to the distance. This creates diamonds problem for products, as the
49 uniform structure on the product of two emetric spaces could be obtained first
50 by obtaining two uniform spaces and then taking their products, or by taking
51 the product of the emetric spaces and then the associated uniform structure.
52 The two uniform structure we have just described are equal, but not defeq, which
53 creates a lot of problem.
54
55 The idea is to add, in the very definition of an `emetric_space`, a uniform structure
56 with a uniformity which equal to the one given by the distance, but maybe not defeq.
57 And the instance from `emetric_space` to `uniform_space` uses this uniformity.
58 In this way, when we create the product of emetric spaces, we put in the product
59 the uniformity corresponding to the product of the uniformities. There is one more
60 proof obligation, that this product uniformity is equal to the uniformity corresponding
61 to the product metric. But the diamond problem disappears.
62
63 The same trick is used in the definition of a metric space, where one stores as well
64 a uniform structure and an edistance. -/
65
66 /-- Creating a uniform space from an extended distance. -/
67 def uniform_space_of_edist
68 (edist : α → α → ennreal)
69 (edist_self : ∀ x : α, edist x x = 0)
70 (edist_comm : ∀ x y : α, edist x y = edist y x)
71 (edist_triangle : ∀ x y z : α, edist x z ≤ edist x y + edist y z) : uniform_space α :=
72 uniform_space.of_core {
73 uniformity := (⨅ ε>0, principal {p:α×α | edist p.1 p.2 < ε}),
74 refl := le_infi $ assume ε, le_infi $
75 by simp [set.subset_def, id_rel, edist_self, (>)] {contextual := tt},
id └┘
src └────┘ └┘ └┘ └┘ └──┘ └────────────┘└┘┴
typ └────┘ └┘ └┘ └┘ └──┘ └────────────┘└┘┴
doc └────┘ └┘ └┘ └┘ └──┘ └────────────┘ ┴
txt └────┘ └┘ └┘ └┘ └──┘ └────────────┘ ┴
par └────┘ └┘ └┘ └┘ └──┘ └────────────┘ ┴
pid ┴┴ └┘ └┘ └┘ └─┘┴ └────────────┘ ┴
st └──────────┘
76 comp :=
77 le_infi $ assume ε, le_infi $ assume h,
id └─────┘ ┴ └─────┘ ┴
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴
78 have (2 : ennreal) = (2 : ℕ) := by simp,
id └─────┘ ┴ ┴
src └─────┘ ┴ ┴ └──┘
typ └─────┘ ┴ ┴ └──┘
doc └─────┘ └──┘
txt └──┘
par └──┘
st └───┘
79 have A : 0 < ε / 2 := ennreal.div_pos_iff.2 ⟨ne_of_gt h, this ▸ ennreal.nat_ne_top 2⟩,
id ┴ ┴ ┴ └─────────────────┘┴ └──────┘ ┴ └──┘ ┴ └────────────────┘
src ┴ ┴ └─────────────────┘┴ └──────┘ ┴ └────────────────┘
typ ┴ ┴ ┴ └─────────────────┘┴ └──────┘ ┴ └──┘ ┴ └────────────────┘
80 lift'_le
id └──────┘
src └──────┘
typ └──────┘
81 (mem_infi_sets (ε / 2) $ mem_infi_sets A (subset.refl _)) $
id └───────────┘ ┴ ┴ └───────────┘ ┴ └─────────┘
src └───────────┘ ┴ └───────────┘ └─────────┘
typ └───────────┘ ┴ ┴ └───────────┘ ┴ └─────────┘
82 have ∀ (a b c : α), edist a c < ε / 2 → edist c b < ε / 2 → edist a b < ε,
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
83 from assume a b c hac hcb,
id ┴ ┴ ┴ └─┘ └─┘
typ ┴ ┴ ┴ └─┘ └─┘
84 calc edist a b ≤ edist a c + edist c b : edist_triangle _ _ _
id └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └────────────┘
src ┴
typ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └────────────┘
85 ... < ε / 2 + ε / 2 : ennreal.add_lt_add hac hcb
id ┴ ┴ ┴ ┴ ┴ └────────────────┘ └─┘ └─┘
src ┴ ┴ ┴ └────────────────┘
typ ┴ ┴ ┴ ┴ ┴ └────────────────┘ └─┘ └─┘
86 ... = ε : by rw [ennreal.add_halves],
id ┴ └────────────────┘
src └──┘└────────────────┘┴
typ ┴ └──┘└────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st └─────────────────────┘┴
87 by simpa [comp_rel],
id └──────┘
src └─────┘└──────┘┴
typ └─────┘└──────┘┴
doc └─────┘└──────┘┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st └───────────────┘
88 symm := tendsto_infi.2 $ assume ε, tendsto_infi.2 $ assume h,
id └──────────┘┴ ┴ └──────────┘┴ ┴
src └──────────┘┴ └──────────┘┴
typ └──────────┘┴ ┴ └──────────┘┴ ┴
89 tendsto_infi' ε $ tendsto_infi' h $ tendsto_principal_principal.2 $ by simp [edist_comm] }
id └───────────┘ ┴ └───────────┘ ┴ └─────────────────────────┘┴ └────────┘
src └───────────┘ └───────────┘ └─────────────────────────┘┴ └────┘ └┘
typ └───────────┘ ┴ └───────────┘ ┴ └─────────────────────────┘┴ └────┘└────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └─────────────────┘
90
91 section prio
92 set_option default_priority 100 -- see Note [default priority]
doc └──────────────┘
93 /-- Extended metric spaces, with an extended distance `edist` possibly taking the
94 value ∞
95
96 Each emetric space induces a canonical `uniform_space` and hence a canonical `topological_space`.
97 This is enforced in the type class definition, by extending the `uniform_space` structure. When
98 instantiating an `emetric_space` structure, the uniformity fields are not necessary, they will be
99 filled in by default. There is a default value for the uniformity, that can be substituted
100 in cases of interest, for instance when instantiating an `emetric_space` structure
101 on a product.
102
103 Continuity of `edist` is finally proving in `topology.instances.ennreal`
104 -/
105 class emetric_space (α : Type u) extends has_edist α : Type u :=
id └──┘ └───────┘ ┴
src └───────┘
typ └──┘ └───────┘ ┴
106 (edist_self : ∀ x : α, edist x x = 0)
id ┴ ┴ └───┘ ┴ ┴ ┴
src ┴
typ ┴ ┴ └───┘ ┴ ┴ ┴
107 (eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y)
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
108 (edist_comm : ∀ x y : α, edist x y = edist y x)
id ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src ┴
typ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
109 (edist_triangle : ∀ x y z : α, edist x z ≤ edist x y + edist y z)
id ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src ┴ ┴
typ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
110 (to_uniform_space : uniform_space α := uniform_space_of_edist edist edist_self edist_comm edist_triangle)
id └───────────┘ ┴ └────────────────────┘ └───┘ └────────┘ └────────┘ └────────────┘
src └───────────┘ └────────────────────┘
typ └───────────┘ ┴ └────────────────────┘ └───┘ └────────┘ └────────┘ └────────────┘
doc └───────────┘ └────────────────────┘
111 (uniformity_edist : 𝓤 α = ⨅ ε>0, principal {p:α×α | edist p.1 p.2 < ε} . control_laws_tac)
id ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴┴┴ └───┘ ┴┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴┴┴ └───┘ ┴┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴ └───────┘
112 end prio
113
114 /- emetric spaces are less common than metric spaces. Therefore, we work in a dedicated
115 namespace, while notions associated to metric spaces are mostly in the root namespace. -/
116 variables [emetric_space α]
id └───────────┘
src └───────────┘
typ └───────────┘
doc └───────────┘
117
118 @[priority 100] -- see Note [lower instance priority]
119 instance emetric_space.to_uniform_space' : uniform_space α :=
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
doc └───────────┘
120 emetric_space.to_uniform_space α
id └────────────────────────────┘ ┴
src └────────────────────────────┘
typ └────────────────────────────┘ ┴
121
122 export emetric_space (edist_self eq_of_edist_eq_zero edist_comm edist_triangle)
123
124 attribute [simp] edist_self
id └────────┘
src └────────┘
typ └────────┘
doc └──┘
125
126 /-- Characterize the equality of points by the vanishing of their extended distance -/
127 @[simp] theorem edist_eq_zero {x y : α} : edist x y = 0 ↔ x = y :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
128 iff.intro eq_of_edist_eq_zero (assume : x = y, this ▸ edist_self _)
id └───────┘ └─────────────────┘ ┴ ┴ ┴ └──┘ ┴ └────────┘
src └───────┘ └─────────────────┘ ┴ ┴ └────────┘
typ └───────┘ └─────────────────┘ ┴ ┴ ┴ └──┘ ┴ └────────┘
129
130 @[simp] theorem zero_eq_edist {x y : α} : 0 = edist x y ↔ x = y :=
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
131 iff.intro (assume h, eq_of_edist_eq_zero (h.symm))
id └───────┘ ┴ └─────────────────┘ ┴└───┘
src └───────┘ └─────────────────┘ └───┘
typ └───────┘ ┴ └─────────────────┘ ┴└───┘
132 (assume : x = y, this ▸ (edist_self _).symm)
id ┴ ┴ ┴ └──┘ ┴ └────────┘ └──┘
src ┴ ┴ └────────┘ └──┘
typ ┴ ┴ ┴ └──┘ ┴ └────────┘ └──┘
133
134 theorem edist_le_zero {x y : α} : (edist x y ≤ 0) ↔ x = y :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
135 le_zero_iff_eq.trans edist_eq_zero
id └────────────┘└────┘ └───────────┘
src └────────────┘└────┘ └───────────┘
typ └────────────┘└────┘ └───────────┘
doc └───────────┘
136
137 /-- Triangle inequality for the extended distance -/
138 theorem edist_triangle_left (x y z : α) : edist x y ≤ edist z x + edist z y :=
id ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └───┘ ┴ └───┘ ┴ └───┘
typ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
139 by rw edist_comm z; apply edist_triangle
id └────────┘ ┴ └────────────┘
src └─┘└────────┘┴ └────┘└────────────┘└
typ └─┘└────────┘┴┴ └────┘└────────────┘└
doc └─┘ ┴ └────┘ └
txt └─┘ ┴ └────┘ └
par └─┘ ┴ └────┘ └
pid ┴ ┴ ┴ └
st └──────────────────────────────────────
140
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
141 theorem edist_triangle_right (x y z : α) : edist x y ≤ edist x z + edist y z :=
id ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └───┘ ┴ └───┘ ┴ └───┘
typ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
142 by rw edist_comm y; apply edist_triangle
id └────────┘ ┴ └────────────┘
src └─┘└────────┘┴ └────┘└────────────┘└
typ └─┘└────────┘┴┴ └────┘└────────────┘└
doc └─┘ ┴ └────┘ └
txt └─┘ ┴ └────┘ └
par └─┘ ┴ └────┘ └
pid ┴ ┴ ┴ └
st └──────────────────────────────────────
143
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
144 lemma edist_triangle4 (x y z t : α) :
id ┴
typ ┴
145 edist x t ≤ edist x y + edist y z + edist z t :=
id └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └───┘ ┴ └───┘ ┴ └───┘ ┴ └───┘
typ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
146 calc
147 edist x t ≤ edist x z + edist z t : edist_triangle x z t
id └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └────────────┘ ┴ ┴ ┴
src └───┘ └───┘ ┴ └───┘ └────────────┘
typ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └────────────┘ ┴ ┴ ┴
148 ... ≤ (edist x y + edist y z) + edist z t : add_le_add_right' (edist_triangle x y z)
id └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └───────────────┘ └────────────┘ ┴ ┴ ┴
src └───┘ ┴ └───┘ ┴ └───┘ └───────────────┘ └────────────┘
typ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └───────────────┘ └────────────┘ ┴ ┴ ┴
149
150 /-- The triangle (polygon) inequality for sequences of points; `finset.Ico` version. -/
151 lemma edist_le_Ico_sum_edist (f : ℕ → α) {m n} (h : m ≤ n) :
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
152 edist (f m) (f n) ≤ (finset.Ico m n).sum (λ i, edist (f i) (f (i + 1))) :=
id └───┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ └────────┘ └─┘ └───┘ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └────────┘
153 begin
st └─────
154 revert n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ─────────┘└─
155 refine nat.le_induction _ _,
id └──────────────┘
src └─────┘└──────────────┘└──┘
typ └─────┘└──────────────┘└──┘
doc └─────┘└──────────────┘└──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ────────────────────────────┘└─
156 { simp only [finset.sum_empty, finset.Ico.self_eq_empty, edist_self],
id └──────────────┘ └──────────────────────┘ └────────┘
src └─────────┘└──────────────┘└┘└──────────────────────┘└┘└────────┘┴
typ └─────────┘└──────────────┘└┘└──────────────────────┘└┘└────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ───┘└────────────────────────────────────────────────────────────────┘└─
157 -- TODO: Why doesn't Lean close this goal automatically? `apply le_refl` fails too.
st ────────────────────────────────────────────────────────────────────────────────────────
158 exact le_refl (0:ennreal) },
id └─────┘ └─────┘
src └────┘└─────┘┴ └┘└─────┘└┘
typ └────┘└─────┘┴ └┘└─────┘└┘
doc └────┘ ┴ └┘└─────┘└┘
txt └────┘ ┴ └┘ └┘
par └────┘ ┴ └┘ └┘
pid ┴ ┴ └┘ ┴┴
st ─────────────────────────────┘└┘└
159 { assume n hn hrec,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └──────────────┘
st ───────────────────┘└─
160 calc edist (f m) (f (n+1)) ≤ edist (f m) (f n) + edist (f n) (f (n+1)) : edist_triangle _ _ _
id └──┘ ┴ ┴ └───┘ ┴ ┴ └────────────┘
src └──┘ ┴ └───┘ └────────────┘
typ └──┘ ┴ ┴ └───┘ ┴ ┴ └────────────┘
doc └──┘
st ──────────────────────────────────────────────────────────────────────────────────────────────────
161 ... ≤ (finset.Ico m n).sum _ + _ : add_le_add' hrec (le_refl _)
id └─┘ └─────────┘ └──┘ └─────┘
src └─┘ └─────────┘ └─────┘
typ └─┘ └─────────┘ └──┘ └─────┘
st ──────────────────────────────────────────────────────────────────────
162 ... = (finset.Ico m (n+1)).sum _ :
id └────────┘ └─┘
src └────────┘ └─┘
typ └────────┘ └─┘
doc └────────┘
st ─────────────────────────────────────────
163 by rw [finset.Ico.succ_top hn, finset.sum_insert, add_comm]; simp }
id └─────────────────┘ └┘ └───────────────┘ └──────┘
src └──┘└─────────────────┘┴ └┘└───────────────┘└┘└──────┘┴ └───┘
typ └──┘└─────────────────┘┴└┘└┘└───────────────┘└┘└──────┘┴ └───┘
doc └──┘ ┴ └┘ └┘ ┴ └───┘
txt └──┘ ┴ └┘ └┘ ┴ └───┘
par └──┘ ┴ └┘ └┘ ┴ └───┘
pid └┘ ┴ └┘ └┘ ┴ ┴
st ─────────┘└─────────────────────────┘└─────────────────┘└────────┘┴└─────┘└─
164 end
st ──┘
165
166 /-- The triangle (polygon) inequality for sequences of points; `finset.range` version. -/
167 lemma edist_le_range_sum_edist (f : ℕ → α) (n : ℕ) :
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
168 edist (f 0) (f n) ≤ (finset.range n).sum (λ i, edist (f i) (f (i + 1))) :=
id └───┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ └──────────┘ └─┘ └───┘ ┴
typ └───┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └──────────┘
169 finset.Ico.zero_bot n ▸ edist_le_Ico_sum_edist f (nat.zero_le n)
id └─────────────────┘ ┴ ┴ └────────────────────┘ ┴ └─────────┘ ┴
src └─────────────────┘ ┴ └────────────────────┘ └─────────┘
typ └─────────────────┘ ┴ ┴ └────────────────────┘ ┴ └─────────┘ ┴
doc └────────────────────┘
170
171 /-- A version of `edist_le_Ico_sum_edist` with each intermediate distance replaced
172 with an upper estimate. -/
173 lemma edist_le_Ico_sum_of_edist_le {f : ℕ → α} {m n} (hmn : m ≤ n)
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
174 {d : ℕ → ennreal} (hd : ∀ {k}, m ≤ k → k < n → edist (f k) (f (k + 1)) ≤ d k) :
id ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─────┘ ┴ ┴ └───┘ ┴ ┴
typ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
175 edist (f m) (f n) ≤ (finset.Ico m n).sum d :=
id └───┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └─┘ ┴
src └───┘ ┴ └────────┘ └─┘
typ └───┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └─┘ ┴
doc └────────┘
176 le_trans (edist_le_Ico_sum_edist f hmn) $
id └──────┘ └────────────────────┘ ┴ └─┘
src └──────┘ └────────────────────┘
typ └──────┘ └────────────────────┘ ┴ └─┘
doc └────────────────────┘
177 finset.sum_le_sum $ λ k hk, hd (finset.Ico.mem.1 hk).1 (finset.Ico.mem.1 hk).2
id └───────────────┘ ┴ └┘ └┘ └────────────┘┴ └┘ ┴ └────────────┘┴ └┘ ┴
src └───────────────┘ └────────────┘┴ ┴ └────────────┘┴ ┴
typ └───────────────┘ ┴ └┘ └┘ └────────────┘┴ └┘ ┴ └────────────┘┴ └┘ ┴
178
179 /-- A version of `edist_le_range_sum_edist` with each intermediate distance replaced
180 with an upper estimate. -/
181 lemma edist_le_range_sum_of_edist_le {f : ℕ → α} (n : ℕ)
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
182 {d : ℕ → ennreal} (hd : ∀ {k}, k < n → edist (f k) (f (k + 1)) ≤ d k) :
id ┴ └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─────┘ ┴ └───┘ ┴ ┴
typ ┴ └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
183 edist (f 0) (f n) ≤ (finset.range n).sum d :=
id └───┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ └─┘ ┴
src └───┘ ┴ └──────────┘ └─┘
typ └───┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ └─┘ ┴
doc └──────────┘
184 finset.Ico.zero_bot n ▸ edist_le_Ico_sum_of_edist_le (zero_le n) (λ _ _, hd)
id └─────────────────┘ ┴ ┴ └──────────────────────────┘ └─────┘ ┴ ┴ ┴ └┘
src └─────────────────┘ ┴ └──────────────────────────┘ └─────┘
typ └─────────────────┘ ┴ ┴ └──────────────────────────┘ └─────┘ ┴ ┴ ┴ └┘
doc └──────────────────────────┘
185
186 /-- Two points coincide if their distance is `< ε` for all positive ε -/
187 theorem eq_of_forall_edist_le {x y : α} (h : ∀ε, ε > 0 → edist x y ≤ ε) : x = y :=
id ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴
typ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
188 eq_of_edist_eq_zero (eq_of_le_of_forall_le_of_dense bot_le h)
id └─────────────────┘ └────────────────────────────┘ └────┘ ┴
src └─────────────────┘ └────────────────────────────┘ └────┘
typ └─────────────────┘ └────────────────────────────┘ └────┘ ┴
189
190 /-- Reformulation of the uniform structure in terms of the extended distance -/
191 theorem uniformity_edist' : 𝓤 α = (⨅ ε>0, principal {p:α×α | edist p.1 p.2 < ε}) :=
id ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴┴┴ └───┘ ┴┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴┴┴ └───┘ ┴┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ └───────┘
192 emetric_space.uniformity_edist _
id └────────────────────────────┘
src └────────────────────────────┘
typ └────────────────────────────┘
193
194 /-- Reformulation of the uniform structure in terms of the extended distance on a subtype -/
195 theorem uniformity_edist'' : 𝓤 α = (⨅ε:{ε:ennreal // ε>0}, principal {p:α×α | edist p.1 p.2 < ε.val}) :=
id ┴ ┴ ┴ ┴ ┴ └─────┘ ┴┴ ┴ └───────┘ ┴ ┴┴┴ └───┘ ┴┴ ┴┴ ┴ ┴└──┘
src ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └───────┘ ┴ ┴ └───┘ ┴ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴┴ ┴ └───────┘ ┴ ┴┴┴ └───┘ ┴┴ ┴┴ ┴ ┴└──┘
doc ┴ ┴ └─────┘ ┴ └───────┘
196 by { simp only [infi_subtype], exact uniformity_edist' }
id └──────────┘ └───────────────┘
src └─────────┘└──────────┘┴ └────┘└───────────────┘┴
typ └─────────┘└──────────┘┴ └────┘└───────────────┘┴
doc └─────────┘ ┴ └────┘└───────────────┘┴
txt └─────────┘ ┴ └────┘ ┴
par └─────────┘ ┴ └────┘ ┴
pid ┴└──┘└┘ ┴ ┴ ┴
st └─────────────────────────┘└────────────────────────┘└┘
197
198 /-- Characterization of the elements of the uniformity in terms of the extended distance -/
199 theorem mem_uniformity_edist {s : set (α×α)} :
id └─┘ ┴┴┴
src └─┘ ┴
typ └─┘ ┴┴┴
200 s ∈ 𝓤 α ↔ (∃ε>0, ∀{a b:α}, edist a b < ε → (a, b) ∈ s) :=
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴
201 begin
st └─────
202 rw [uniformity_edist'', mem_infi],
id └────────────────┘ └──────┘
src └──┘└────────────────┘└┘└──────┘┴
typ └──┘└────────────────┘└┘└──────┘┴
doc └──┘└────────────────┘└┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────────────────┘└────────┘└──
203 simp [subset_def],
id └────────┘
src └────┘└────────┘┴
typ └────┘└────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ──────────────────┘└─
204 exact assume ⟨r, hr⟩ ⟨p, hp⟩, ⟨⟨min r p, lt_min hr hp⟩, by simp [lt_min_iff, (≥)] {contextual := tt}⟩,
id ┴ └┘ ┴ └┘ └─┘ └────┘ └────────┘ ┴ └┘
src └────┘ └┘ └┘ └─┘ └┘ └─┘ └─┘┴ ┴ └┘└────┘┴ ┴ └─┘ ┴└────┘└────────┘└┘┴└──┘ └────────────┘└┘┴┴
typ └────┘ └┘┴└┘└┘└─┘┴└┘└┘└─┘ └─┘┴ ┴ └┘└────┘┴ ┴ └─┘ ┴└────┘└────────┘└┘┴└──┘ └────────────┘└┘┴┴
doc └────┘ └┘ └┘ └─┘ └┘ └─┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴└────┘ └┘ └──┘ └────────────┘ ┴┴
txt └────┘ └┘ └┘ └─┘ └┘ └─┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴└────┘ └┘ └──┘ └────────────┘ ┴┴
par └────┘ └┘ └┘ └─┘ └┘ └─┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴└────┘ └┘ └──┘ └────────────┘ ┴┴
pid ┴ └┘ └┘ └─┘ └┘ └─┘ ┴ ┴ └┘ ┴ ┴ └─┘ └─────┘ └┘ └──┘ └────────────┘ └┘
st ───────────────────────────────────────────────────────────┘└────────────────────────────────────────┘┴└─
205 exact ⟨⟨1, ennreal.zero_lt_one⟩⟩
id └─────────────────┘
src └────┘ └─┘└─────────────────┘└─┘
typ └────┘ └─┘└─────────────────┘└─┘
doc └────┘ └─┘ └─┘
txt └────┘ └─┘ └─┘
par └────┘ └─┘ └─┘
pid ┴ └─┘ └┘┴
st ──────────────────────────────────┘
206 end
st └─┘
207
208 /-- Fixed size neighborhoods of the diagonal belong to the uniform structure -/
209 theorem edist_mem_uniformity {ε:ennreal} (ε0 : 0 < ε) :
id └─────┘ ┴ ┴
src └─────┘ ┴
typ └─────┘ ┴ ┴
doc └─────┘
210 {p:α×α | edist p.1 p.2 < ε} ∈ 𝓤 α :=
id ┴ ┴┴┴ └───┘ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴┴ └───┘ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴
doc ┴
211 mem_uniformity_edist.2 ⟨ε, ε0, λ a b, id⟩
id └──────────────────┘┴ ┴ └┘ ┴ ┴ └┘
src └──────────────────┘┴ └┘
typ └──────────────────┘┴ ┴ └┘ ┴ ┴ └┘
doc └──────────────────┘
212
213 theorem uniformity_edist_nnreal :
214 𝓤 α = (⨅(ε:nnreal) (h : ε > 0), principal {p:α×α | edist p.1 p.2 < ε}) :=
id ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └───────┘ ┴ ┴┴┴ └───┘ ┴┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ └────┘ ┴ ┴ └───────┘ ┴ ┴ └───┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └───────┘ ┴ ┴┴┴ └───┘ ┴┴ ┴┴ ┴ ┴
doc ┴ ┴ └────┘ ┴ └───────┘
215 begin
st └─────
216 rw [uniformity_edist', ennreal.infi_ennreal, inf_of_le_left],
id └───────────────┘ └──────────────────┘ └────────────┘
src └──┘└───────────────┘└┘└──────────────────┘└┘└────────────┘┴
typ └──┘└───────────────┘└┘└──────────────────┘└┘└────────────┘┴
doc └──┘└───────────────┘└┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ──────────────────────┘└────────────────────┘└──────────────┘└──
217 { congr, funext ε, refine infi_congr_Prop ennreal.coe_pos _, assume h, refl },
id └─────────────┘ └─────────────┘
src └───┘ └──────┘ └─────┘└─────────────┘┴└─────────────┘└┘ └──────┘ └───┘
typ └───┘ └──────┘ └─────┘└─────────────┘┴└─────────────┘└┘ └──────┘ └───┘
doc └──────┘ └─────┘ ┴ └┘ └──────┘ └───┘
txt └───┘ └──────┘ └─────┘ ┴ └┘ └──────┘ └───┘
par └───┘ └──────┘ └─────┘ ┴ └┘ └──────┘ └───┘
pid └┘ ┴ ┴ └┘ └──────┘ ┴
st ───┘└───┘└────────┘└────────────────────────────────────────┘└────────┘└─────┘└┘└
218 refine le_infi (assume h, infi_le_of_le 1 $ infi_le_of_le ennreal.zero_lt_one $ _),
id └─────┘ └───────────┘ └─────────────────┘
src └─────┘└─────┘┴ └──┘ └─┘ ┴└───────────┘┴└─────────────────┘┴ └─┘
typ └─────┘└─────┘┴ └──┘ └─┘ ┴└───────────┘┴└─────────────────┘┴ └─┘
doc └─────┘ ┴ └──┘ └─┘ ┴ ┴ ┴ └─┘
txt └─────┘ ┴ └──┘ └─┘ ┴ ┴ ┴ └─┘
par └─────┘ ┴ └──┘ └─┘ ┴ ┴ ┴ └─┘
pid ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ └─┘
st ───────────────────────────────────────────────────────────────────────────────────┘└─
219 exact principal_mono.2 (assume p h, lt_of_lt_of_le h le_top)
id └────────────┘ └────────────┘ └────┘
src └────┘└────────────┘└─┘ └────┘└────────────┘┴ ┴└────┘└┘
typ └────┘└────────────┘└─┘ └────┘└────────────┘┴ ┴└────┘└┘
doc └────┘ └─┘ └────┘ ┴ ┴ └┘
txt └────┘ └─┘ └────┘ ┴ ┴ └┘
par └────┘ └─┘ └────┘ ┴ ┴ └┘
pid ┴ └─┘ └────┘ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────────────────┘
220 end
st └─┘
221
222 theorem mem_uniformity_edist_inv_nat {s : set (α×α)} :
id └─┘ ┴┴┴
src └─┘ ┴
typ └─┘ ┴┴┴
223 s ∈ 𝓤 α ↔ (∃n:ℕ, ∀ a b : α, edist a b < n⁻¹ → (a, b) ∈ s) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └───┘ ┴ ┴ ┴ ┴└┘ ┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴┴ └───┘ ┴ └┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └───┘ ┴ ┴ ┴ ┴└┘ ┴┴ ┴ ┴ ┴
doc ┴
224 begin
st └─────
225 refine mem_uniformity_edist.trans ⟨λ hs, _, λ hs, _⟩,
id └────────────────────────┘
src └─────┘└────────────────────────┘┴ └──────┘ └─────┘
typ └─────┘└────────────────────────┘┴ └──────┘ └─────┘
doc └─────┘└────────────────────────┘┴ └──────┘ └─────┘
txt └─────┘ ┴ └──────┘ └─────┘
par └─────┘ ┴ └──────┘ └─────┘
pid ┴ ┴ └──────┘ └─────┘
st ─────────────────────────────────────────────────────┘└─
226 { rcases hs with ⟨ε, ε_pos, hε⟩,
id └┘
src └─────┘ └──────────────────┘
typ └─────┘└┘└──────────────────┘
doc └─────┘ └──────────────────┘
txt └─────┘ └──────────────────┘
par └─────┘ └──────────────────┘
pid ┴ └──────────────────┘
st ───┘└───────────────────────────┘└─
227 rcases ennreal.exists_inv_nat_lt (ne_of_gt ε_pos) with ⟨n, hn⟩,
id └───────────────────────┘ └──────┘ └───┘
src └─────┘└───────────────────────┘┴ └──────┘┴ └────────────┘
typ └─────┘└───────────────────────┘┴ └──────┘┴└───┘└────────────┘
doc └─────┘ ┴ ┴ └────────────┘
txt └─────┘ ┴ ┴ └────────────┘
par └─────┘ ┴ ┴ └────────────┘
pid ┴ ┴ ┴ └────────────┘
st ─────────────────────────────────────────────────────────────────┘└─
228 exact ⟨n, λ a b hab, hε (lt_trans hab hn)⟩ },
id ┴ └┘ └──────┘ └┘
src └────┘ └┘ └────────┘ ┴ └──────┘┴ ┴ └─┘
typ └────┘ ┴└┘ └────────┘└┘┴ └──────┘┴ ┴└┘└─┘
doc └────┘ └┘ └────────┘ ┴ ┴ ┴ └─┘
txt └────┘ └┘ └────────┘ ┴ ┴ ┴ └─┘
par └────┘ └┘ └────────┘ ┴ ┴ ┴ └─┘
pid ┴ └┘ └────────┘ ┴ ┴ ┴ └┘┴
st ──────────────────────────────────────────────┘└┘└
229 { rcases hs with ⟨n, hn⟩,
id └┘
src └─────┘ └───────────┘
typ └─────┘└┘└───────────┘
doc └─────┘ └───────────┘
txt └─────┘ └───────────┘
par └─────┘ └───────────┘
pid ┴ └───────────┘
st ─────────────────────────┘└─
230 exact ⟨n⁻¹, ennreal.inv_pos.2 ennreal.coe_nat_ne_top, hn⟩ }
id ┴└┘ └─────────────┘ └────────────────────┘ └┘
src └────┘ └┘└┘└─────────────┘└─┘└────────────────────┘└┘ └┘
typ └────┘ ┴└┘└┘└─────────────┘└─┘└────────────────────┘└┘└┘└┘
doc └────┘ └┘ └─┘ └┘ └┘
txt └────┘ └┘ └─┘ └┘ └┘
par └────┘ └┘ └─┘ └┘ └┘
pid ┴ └┘ └─┘ └┘ ┴┴
st ─────────────────────────────────────────────────────────────┘└─
231 end
st ──┘
232
233 theorem uniformity_edist_inv_nat :
234 𝓤 α = (⨅ n:ℕ, principal {p:α×α | edist p.1 p.2 < n⁻¹}) :=
id ┴ ┴ ┴ ┴ ┴┴ └───────┘ ┴ ┴┴┴ └───┘ ┴┴ ┴┴ ┴ ┴└┘
src ┴ ┴ ┴ ┴┴ └───────┘ ┴ ┴ └───┘ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴┴ └───────┘ ┴ ┴┴┴ └───┘ ┴┴ ┴┴ ┴ ┴└┘
doc ┴ ┴ ┴ └───────┘
235 begin
st └─────
236 refine eq_infi_of_mem_sets_iff_exists_mem (λ s, mem_uniformity_edist_inv_nat.trans _),
id └────────────────────────────────┘ └────────────────────────────────┘
src └─────┘└────────────────────────────────┘┴ └──┘└────────────────────────────────┘└─┘
typ └─────┘└────────────────────────────────┘┴ └──┘└────────────────────────────────┘└─┘
doc └─────┘ ┴ └──┘ └─┘
txt └─────┘ ┴ └──┘ └─┘
par └─────┘ ┴ └──┘ └─┘
pid ┴ ┴ └──┘ └─┘
st ──────────────────────────────────────────────────────────────────────────────────────┘└─
237 exact exists_congr (λn, by simp only [prod.forall, mem_principal_sets, subset_def, mem_set_of_eq])
id └──────────┘ └─────────┘ └────────────────┘ └────────┘ └───────────┘
src └────┘└──────────┘┴ └─┘ ┴└─────────┘└─────────┘└┘└────────────────┘└┘└────────┘└┘└───────────┘┴└┘
typ └────┘└──────────┘┴ └─┘ ┴└─────────┘└─────────┘└┘└────────────────┘└┘└────────┘└┘└───────────┘┴└┘
doc └────┘ ┴ └─┘ ┴└─────────┘ └┘ └┘ └┘ ┴└┘
txt └────┘ ┴ └─┘ ┴└─────────┘ └┘ └┘ └┘ ┴└┘
par └────┘ ┴ └─┘ ┴└─────────┘ └┘ └┘ └┘ ┴└┘
pid ┴ ┴ └─┘ └──────────┘ └┘ └┘ └┘ └┘┴
st ───────────────────────────┘└─────────────────────────────────────────────────────────────────────┘└┘
238 end
st └─┘
239
240 namespace emetric
241
242 theorem uniformity_has_countable_basis : has_countable_basis (𝓤 α) :=
id └─────────────────┘ ┴ ┴
src └─────────────────┘ ┴
typ └─────────────────┘ ┴ ┴
doc └─────────────────┘ ┴
243 has_countable_basis_of_seq _ _ uniformity_edist_inv_nat
id └────────────────────────┘ └──────────────────────┘
src └────────────────────────┘ └──────────────────────┘
typ └────────────────────────┘ └──────────────────────┘
244
245 /-- ε-δ characterization of uniform continuity on emetric spaces -/
246 theorem uniform_continuous_iff [emetric_space β] {f : α → β} :
id └───────────┘ ┴ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴ ┴
doc └───────────┘
247 uniform_continuous f ↔ ∀ ε > 0, ∃ δ > 0,
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴ ┴ ┴ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
248 ∀{a b:α}, edist a b < δ → edist (f a) (f b) < ε :=
id ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ └───┘ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
249 uniform_continuous_def.trans
id └────────────────────┘└────┘
src └────────────────────┘└────┘
typ └────────────────────┘└────┘
250 ⟨λ H ε ε0, mem_uniformity_edist.1 $ H _ $ edist_mem_uniformity ε0,
id ┴ ┴ └┘ └──────────────────┘┴ ┴ └──────────────────┘ └┘
src └──────────────────┘┴ └──────────────────┘
typ ┴ ┴ └┘ └──────────────────┘┴ ┴ └──────────────────┘ └┘
doc └──────────────────┘ └──────────────────┘
251 λ H r ru,
id ┴ ┴ └┘
typ ┴ ┴ └┘
252 let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru, ⟨δ, δ0, hδ⟩ := H _ ε0 in
id └─┘ └┘ └┘ └──────────────────┘┴ └┘ ┴ └┘ └┘ ┴
src └──────────────────┘┴
typ └─┘ └┘ └┘ └──────────────────┘┴ └┘ ┴ └┘ └┘ ┴
doc └──────────────────┘
253 mem_uniformity_edist.2 ⟨δ, δ0, λ a b h, hε (hδ h)⟩⟩
id └──────────────────┘┴ ┴ ┴ ┴ ┴
src └──────────────────┘┴
typ └──────────────────┘┴ ┴ ┴ ┴ ┴
doc └──────────────────┘
254
255 /-- ε-δ characterization of uniform embeddings on emetric spaces -/
256 theorem uniform_embedding_iff [emetric_space β] {f : α → β} :
id └───────────┘ ┴ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴ ┴
doc └───────────┘
257 uniform_embedding f ↔ function.injective f ∧ uniform_continuous f ∧
id └───────────────┘ ┴ ┴ └────────────────┘ ┴ ┴ └────────────────┘ ┴ ┴
src └───────────────┘ ┴ └────────────────┘ ┴ └────────────────┘ ┴
typ └───────────────┘ ┴ ┴ └────────────────┘ ┴ ┴ └────────────────┘ ┴ ┴
258 ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ :=
id ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src ┴ ┴ └───┘ ┴ └───┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
259 uniform_embedding_def'.trans $ and_congr iff.rfl $ and_congr iff.rfl
id └────────────────────┘└────┘ └───────┘ └─────┘ └───────┘ └─────┘
src └────────────────────┘└────┘ └───────┘ └─────┘ └───────┘ └─────┘
typ └────────────────────┘└────┘ └───────┘ └─────┘ └───────┘ └─────┘
260 ⟨λ H δ δ0, let ⟨t, tu, ht⟩ := H _ (edist_mem_uniformity δ0),
id ┴ ┴ └┘ └─┘ └┘ └┘ ┴ └──────────────────┘ └┘
src └──────────────────┘
typ ┴ ┴ └┘ └─┘ └┘ └┘ ┴ └──────────────────┘ └┘
doc └──────────────────┘
261 ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 tu in
id ┴ └┘ └┘ └──────────────────┘┴
src └──────────────────┘┴
typ ┴ └┘ └┘ └──────────────────┘┴
doc └──────────────────┘
262 ⟨ε, ε0, λ a b h, ht _ _ (hε h)⟩,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
263 λ H s su, let ⟨δ, δ0, hδ⟩ := mem_uniformity_edist.1 su, ⟨ε, ε0, hε⟩ := H _ δ0 in
id ┴ ┴ └┘ └─┘ └┘ └┘ └──────────────────┘┴ └┘ └┘ └┘ ┴
src └──────────────────┘┴
typ ┴ ┴ └┘ └─┘ └┘ └┘ └──────────────────┘┴ └┘ └┘ └┘ ┴
doc └──────────────────┘
264 ⟨_, edist_mem_uniformity ε0, λ a b h, hδ (hε h)⟩⟩
id └──────────────────┘ ┴ ┴ ┴ ┴
src └──────────────────┘
typ └──────────────────┘ ┴ ┴ ┴ ┴
doc └──────────────────┘
265
266 /-- A map between emetric spaces is a uniform embedding if and only if the edistance between `f x`
267 and `f y` is controlled in terms of the distance between `x` and `y` and conversely. -/
268 theorem uniform_embedding_iff' [emetric_space β] {f : α → β} :
id └───────────┘ ┴ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴ ┴
doc └───────────┘
269 uniform_embedding f ↔
id └───────────────┘ ┴ ┴
src └───────────────┘ ┴
typ └───────────────┘ ┴ ┴
270 (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε) ∧
id ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └───┘ ┴ └───┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
271 (∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ) :=
id ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src ┴ ┴ └───┘ ┴ └───┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
272 begin
st └─────
273 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
274 { assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
275 exact ⟨uniform_continuous_iff.1 (uniform_embedding_iff.1 h).2.1,
id └────────────────────┘
src └────┘ └────────────────────┘└─┘ └─┘ └──────
typ └────┘ └────────────────────┘└─┘ └─┘ └──────
doc └────┘ └────────────────────┘└─┘ └─┘ └──────
txt └────┘ └─┘ └─┘ └──────
par └────┘ └─┘ └─┘ └──────
pid ┴ └─┘ └─┘ └──────
st ─────────────────────────────────────────────────────────────────────
276 (uniform_embedding_iff.1 h).2.2⟩ },
id └───────────────────┘ ┴
src ─────────┘ └───────────────────┘└─┘ └─────┘
typ ─────────┘ └───────────────────┘└─┘┴└─────┘
doc ─────────┘ └───────────────────┘└─┘ └─────┘
txt ─────────┘ └─┘ └─────┘
par ─────────┘ └─┘ └─────┘
pid ─────────┘ └─┘ └────┘┴
st ──────────────────────────────────────────┘└┘└
277 { rintros ⟨h₁, h₂⟩,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └───────┘
st ───────────────────┘└─
278 refine uniform_embedding_iff.2 ⟨_, uniform_continuous_iff.2 h₁, h₂⟩,
id └───────────────────┘ └────────────────────┘ └┘ └┘
src └─────┘└───────────────────┘└─┘ └─┘└────────────────────┘└─┘ └┘ ┴
typ └─────┘└───────────────────┘└─┘ └─┘└────────────────────┘└─┘└┘└┘└┘┴
doc └─────┘└───────────────────┘└─┘ └─┘└────────────────────┘└─┘ └┘ ┴
txt └─────┘ └─┘ └─┘ └─┘ └┘ ┴
par └─────┘ └─┘ └─┘ └─┘ └┘ ┴
pid ┴ └─┘ └─┘ └─┘ └┘ ┴
st ──────────────────────────────────────────────────────────────────────┘└─
279 assume x y hxy,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ─────────────────┘└─
280 have : edist x y ≤ 0,
id └───┘ ┴ ┴ ┴
src └─────┘└───┘┴ ┴ ┴┴└┘
typ └─────┘└───┘┴┴┴┴┴┴└┘
doc └─────┘ ┴ ┴ ┴ └┘
txt └─────┘ ┴ ┴ ┴ └┘
par └─────┘ ┴ ┴ ┴ └┘
pid └───┘└┘ ┴ ┴ ┴ ┴┴
st ───────────────────────┘└─
281 { refine le_of_forall_lt' (λδ δpos, _),
id └──────────────┘
src └─────┘└──────────────┘┴ └────────┘
typ └─────┘└──────────────┘┴ └────────┘
doc └─────┘ ┴ └────────┘
txt └─────┘ ┴ └────────┘
par └─────┘ ┴ └────────┘
pid ┴ ┴ └────────┘
st ─────┘└──────────────────────────────────┘└─
282 rcases h₂ δ δpos with ⟨ε, εpos, hε⟩,
id └┘ ┴ └──┘
src └─────┘ ┴ ┴ └─────────────────┘
typ └─────┘└┘┴┴┴└──┘└─────────────────┘
doc └─────┘ ┴ ┴ └─────────────────┘
txt └─────┘ ┴ ┴ └─────────────────┘
par └─────┘ ┴ ┴ └─────────────────┘
pid ┴ ┴ ┴ └─────────────────┘
st ────────────────────────────────────────┘└─
283 have : edist (f x) (f y) < ε, by simpa [hxy],
id └───┘ ┴ ┴ ┴ ┴ ┴ └─┘
src └─────┘└───┘┴ ┴ └┘ ┴ └┘┴┴ └─────┘ ┴
typ └─────┘└───┘┴ ┴┴└┘ ┴┴┴└┘┴┴┴ └─────┘└─┘┴
doc └─────┘ ┴ ┴ └┘ ┴ └┘ ┴ └─────┘ ┴
txt └─────┘ ┴ ┴ └┘ ┴ └┘ ┴ └─────┘ ┴
par └─────┘ ┴ ┴ └┘ ┴ └┘ ┴ └─────┘ ┴
pid └───┘└┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴┴ ┴
st ─────────────────────────────────┘ └─
284 exact hε this },
id └┘ └──┘
src └────┘ ┴ ┴
typ └────┘└┘┴└──┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ───────────────────┘└┘└
285 simpa using this }
id └──┘
src └──────────┘ ┴
typ └──────────┘└──┘┴
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid ┴└────┘ ┴
st ────────────────────┘└─
286 end
st ──┘
287
288 /-- ε-δ characterization of Cauchy sequences on emetric spaces -/
289 protected lemma cauchy_iff {f : filter α} :
id └────┘ ┴
src └────┘
typ └────┘ ┴
290 cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x y ∈ t, edist x y < ε :=
id └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
typ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
doc └────┘
291 cauchy_iff.trans $ and_congr iff.rfl
id └────────┘└────┘ └───────┘ └─────┘
src └────────┘└────┘ └───────┘ └─────┘
typ └────────┘└────┘ └───────┘ └─────┘
292 ⟨λ H ε ε0, let ⟨t, tf, ts⟩ := H _ (edist_mem_uniformity ε0) in
id ┴ ┴ └┘ └─┘ ┴ └┘ └┘ ┴ └──────────────────┘ └┘
src └──────────────────┘
typ ┴ ┴ └┘ └─┘ ┴ └┘ └┘ ┴ └──────────────────┘ └┘
doc └──────────────────┘
293 ⟨t, tf, λ x y xt yt, @ts (x, y) ⟨xt, yt⟩⟩,
id ┴ ┴ └┘ └┘ ┴┴ ┴ └┘ └┘
src ┴
typ ┴ ┴ └┘ └┘ ┴┴ ┴ └┘ └┘
294 λ H r ru, let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru,
id ┴ ┴ └┘ └─┘ ┴ └┘ └┘ └──────────────────┘┴ └┘
src └──────────────────┘┴
typ ┴ ┴ └┘ └─┘ ┴ └┘ └┘ └──────────────────┘┴ └┘
doc └──────────────────┘
295 ⟨t, tf, h⟩ := H ε ε0 in
id ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴
296 ⟨t, tf, λ ⟨x, y⟩ ⟨hx, hy⟩, hε (h x y hx hy)⟩⟩
id ┴┴ ┴ ┴└┘ └┘
typ ┴┴ ┴ ┴└┘ └┘
297
298 /-- A very useful criterion to show that a space is complete is to show that all sequences
299 which satisfy a bound of the form `edist (u n) (u m) < B N` for all `n m ≥ N` are
300 converging. This is often applied for `B N = 2^{-N}`, i.e., with a very fast convergence to
301 `0`, which makes it possible to use arguments of converging series, while this is impossible
302 to do in general for arbitrary Cauchy sequences. -/
303 theorem complete_of_convergent_controlled_sequences (B : ℕ → ennreal) (hB : ∀n, 0 < B n)
id ┴ └─────┘ ┴ ┴ ┴ ┴
src ┴ └─────┘ ┴
typ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘
304 (H : ∀u : ℕ → α, (∀N n m : ℕ, N ≤ n → N ≤ m → edist (u n) (u m) < B N) → ∃x, tendsto u at_top (𝓝 x)) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ └─────┘ ┴ └────┘ ┴ ┴
src ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─────┘ └────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ └─────┘ ┴ └────┘ ┴ ┴
doc └─────┘ └────┘ ┴
305 complete_space α :=
id └────────────┘ ┴
src └────────────┘
typ └────────────┘ ┴
doc └────────────┘
306 uniform_space.complete_of_convergent_controlled_sequences
id └───────────────────────────────────────────────────────┘
src └───────────────────────────────────────────────────────┘
typ └───────────────────────────────────────────────────────┘
doc └───────────────────────────────────────────────────────┘
307 uniformity_has_countable_basis
id └────────────────────────────┘
src └────────────────────────────┘
typ └────────────────────────────┘
308 (λ n, {p:α×α | edist p.1 p.2 < B n}) (λ n, edist_mem_uniformity $ hB n) H
id ┴ ┴ ┴┴┴ └───┘ ┴┴ ┴┴ ┴ ┴ ┴ ┴ └──────────────────┘ └┘ ┴ ┴
src ┴ ┴ └───┘ ┴ ┴ ┴ └──────────────────┘
typ ┴ ┴ ┴┴┴ └───┘ ┴┴ ┴┴ ┴ ┴ ┴ ┴ └──────────────────┘ └┘ ┴ ┴
doc └──────────────────┘
309
310 /-- A sequentially complete emetric space is complete. -/
311 theorem complete_of_cauchy_seq_tendsto :
312 (∀ u : ℕ → α, cauchy_seq u → ∃a, tendsto u at_top (𝓝 a)) → complete_space α :=
id ┴ ┴ ┴ ┴ └────────┘ ┴ ┴┴┴ └─────┘ ┴ └────┘ ┴ ┴ └────────────┘ ┴
src ┴ └────────┘ ┴ ┴ └─────┘ └────┘ ┴ └────────────┘
typ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴┴┴ └─────┘ ┴ └────┘ ┴ ┴ └────────────┘ ┴
doc └────────┘ └─────┘ └────┘ ┴ └────────────┘
313 uniform_space.complete_of_cauchy_seq_tendsto uniformity_has_countable_basis
id └──────────────────────────────────────────┘ └────────────────────────────┘
src └──────────────────────────────────────────┘ └────────────────────────────┘
typ └──────────────────────────────────────────┘ └────────────────────────────┘
doc └──────────────────────────────────────────┘
314
315 end emetric
316
317 open emetric
318
319 /-- An emetric space is separated -/
320 @[priority 100] -- see Note [lower instance priority]
321 instance to_separated : separated α :=
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
322 separated_def.2 $ λ x y h, eq_of_forall_edist_le $
id └───────────┘┴ ┴ ┴ ┴ └───────────────────┘
src └───────────┘┴ └───────────────────┘
typ └───────────┘┴ ┴ ┴ ┴ └───────────────────┘
doc └───────────────────┘
323 λ ε ε0, le_of_lt (h _ (edist_mem_uniformity ε0))
id ┴ └┘ └──────┘ ┴ └──────────────────┘ └┘
src └──────┘ └──────────────────┘
typ ┴ └┘ └──────┘ ┴ └──────────────────┘ └┘
doc └──────────────────┘
324
325 /-- Auxiliary function to replace the uniformity on an emetric space with
326 a uniformity which is equal to the original one, but maybe not defeq.
327 This is useful if one wants to construct an emetric space with a
328 specified uniformity. -/
329 def emetric_space.replace_uniformity {α} [U : uniform_space α] (m : emetric_space α)
id └───────────┘ ┴ └───────────┘ ┴
src └───────────┘ └───────────┘
typ └───────────┘ ┴ └───────────┘ ┴
doc └───────────┘ └───────────┘
330 (H : @uniformity _ U = @uniformity _ (emetric_space.to_uniform_space α)) :
id └────────┘ ┴ ┴ └────────┘ └────────────────────────────┘ ┴
src └────────┘ ┴ └────────┘ └────────────────────────────┘
typ └────────┘ ┴ ┴ └────────┘ └────────────────────────────┘ ┴
doc └────────┘ └────────┘
331 emetric_space α :=
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
doc └───────────┘
332 { edist := @edist _ m.to_has_edist,
id └───┘ ┴└───────────┘
src └───┘ └───────────┘
typ └───┘ ┴└───────────┘
333 edist_self := edist_self,
id └────────┘
src └────────┘
typ └────────┘
334 eq_of_edist_eq_zero := @eq_of_edist_eq_zero _ _,
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
335 edist_comm := edist_comm,
id └────────┘
src └────────┘
typ └────────┘
336 edist_triangle := edist_triangle,
id └────────────┘
src └────────────┘
typ └────────────┘
337 to_uniform_space := U,
id ┴
typ ┴
338 uniformity_edist := H.trans (@emetric_space.uniformity_edist α _) }
id ┴└────┘ └────────────────────────────┘ ┴
src └────┘ └────────────────────────────┘
typ ┴└────┘ └────────────────────────────┘ ┴
339
340 /-- The extended metric induced by an injective function taking values in an emetric space. -/
341 def emetric_space.induced {α β} (f : α → β) (hf : function.injective f)
id ┴ ┴ └────────────────┘ ┴
src └────────────────┘
typ ┴ ┴ └────────────────┘ ┴
342 (m : emetric_space β) : emetric_space α :=
id └───────────┘ ┴ └───────────┘ ┴
src └───────────┘ └───────────┘
typ └───────────┘ ┴ └───────────┘ ┴
doc └───────────┘ └───────────┘
343 { edist := λ x y, edist (f x) (f y),
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src └───┘
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
344 edist_self := λ x, edist_self _,
id ┴ └────────┘
src └────────┘
typ ┴ └────────┘
345 eq_of_edist_eq_zero := λ x y h, hf (edist_eq_zero.1 h),
id ┴ ┴ ┴ └┘ └───────────┘┴ ┴
src └───────────┘┴
typ ┴ ┴ ┴ └┘ └───────────┘┴ ┴
doc └───────────┘
346 edist_comm := λ x y, edist_comm _ _,
id ┴ ┴ └────────┘
src └────────┘
typ ┴ ┴ └────────┘
347 edist_triangle := λ x y z, edist_triangle _ _ _,
id ┴ ┴ ┴ └────────────┘
src └────────────┘
typ ┴ ┴ ┴ └────────────┘
348 to_uniform_space := uniform_space.comap f m.to_uniform_space,
id └─────────────────┘ ┴ ┴└───────────────┘
src └─────────────────┘ └───────────────┘
typ └─────────────────┘ ┴ ┴└───────────────┘
doc └─────────────────┘
349 uniformity_edist := begin
st └─────
350 apply @uniformity_dist_of_mem_uniformity _ _ _ _ _ (λ x y, edist (f x) (f y)),
id └───────────────────────────────┘ └───┘ ┴
src └────┘ └───────────────────────────────┘└─────────┘ └────┘└───┘┴ ┴ └┘ ┴ └┘
typ └────┘ └───────────────────────────────┘└─────────┘ └────┘└───┘┴ ┴ └┘ ┴┴ └┘
doc └────┘ └───────────────────────────────┘└─────────┘ └────┘ ┴ ┴ └┘ ┴ └┘
txt └────┘ └─────────┘ └────┘ ┴ ┴ └┘ ┴ └┘
par └────┘ └─────────┘ └────┘ ┴ ┴ └┘ ┴ └┘
pid ┴ └─────────┘ └────┘ ┴ ┴ └┘ ┴ └┘
st ────────────────────────────────────────────────────────────────────────────────┘└─
351 refine λ s, mem_comap_sets.trans _,
id └──────────────────┘
src └─────┘ └──┘└──────────────────┘└┘
typ └─────┘ └──┘└──────────────────┘└┘
doc └─────┘ └──┘ └┘
txt └─────┘ └──┘ └┘
par └─────┘ └──┘ └┘
pid ┴ └──┘ └┘
st ─────────────────────────────────────┘└─
352 split; intro H,
src └───┘ └─────┘
typ └───┘ └─────┘
doc └───┘ └─────┘
txt └───┘ └─────┘
par └───┘ └─────┘
pid └┘
st ─────────────────┘└─
353 { rcases H with ⟨r, ru, rs⟩,
id ┴
src └─────┘ └───────────────┘
typ └─────┘┴└───────────────┘
doc └─────┘ └───────────────┘
txt └─────┘ └───────────────┘
par └─────┘ └───────────────┘
pid ┴ └───────────────┘
st ─────┘└───────────────────────┘└─
354 rcases mem_uniformity_edist.1 ru with ⟨ε, ε0, hε⟩,
id └──────────────────┘ └┘
src └─────┘└──────────────────┘└─┘ └───────────────┘
typ └─────┘└──────────────────┘└─┘└┘└───────────────┘
doc └─────┘└──────────────────┘└─┘ └───────────────┘
txt └─────┘ └─┘ └───────────────┘
par └─────┘ └─┘ └───────────────┘
pid ┴ └─┘ └───────────────┘
st ──────────────────────────────────────────────────────┘└─
355 refine ⟨ε, ε0, λ a b h, rs (hε _)⟩, exact h },
id ┴ └┘ └┘ └┘ ┴
src └─────┘ └┘ └┘ └──────┘ ┴ └──┘ └────┘ ┴
typ └─────┘ ┴└┘└┘└┘ └──────┘└┘┴ └┘└──┘ └────┘┴┴
doc └─────┘ └┘ └┘ └──────┘ ┴ └──┘ └────┘ ┴
txt └─────┘ └┘ └┘ └──────┘ ┴ └──┘ └────┘ ┴
par └─────┘ └┘ └┘ └──────┘ ┴ └──┘ └────┘ ┴
pid ┴ └┘ └┘ └──────┘ ┴ └──┘ ┴ ┴
st ───────────────────────────────────────┘└────────┘└┘└
356 { rcases H with ⟨ε, ε0, hε⟩,
id ┴
src └─────┘ └───────────────┘
typ └─────┘┴└───────────────┘
doc └─────┘ └───────────────┘
txt └─────┘ └───────────────┘
par └─────┘ └───────────────┘
pid ┴ └───────────────┘
st ──────────────────────────────┘└─
357 exact ⟨_, edist_mem_uniformity ε0, λ ⟨a, b⟩, hε⟩ }
id └──────────────────┘ └┘ └┘
src └────┘ └─┘└──────────────────┘┴ └┘ └┘ └┘ └─┘ └┘
typ └────┘ └─┘└──────────────────┘┴└┘└┘ └┘ └┘ └─┘└┘└┘
doc └────┘ └─┘└──────────────────┘┴ └┘ └┘ └┘ └─┘ └┘
txt └────┘ └─┘ ┴ └┘ └┘ └┘ └─┘ └┘
par └────┘ └─┘ ┴ └┘ └┘ └┘ └─┘ └┘
pid ┴ └─┘ ┴ └┘ └┘ └┘ └─┘ ┴┴
st ──────────────────────────────────────────────────────┘└─
358 end }
st ────┘
359
360 /-- Emetric space instance on subsets of emetric spaces -/
361 instance {α : Type*} {p : α → Prop} [t : emetric_space α] : emetric_space (subtype p) :=
id ┴ └───────────┘ ┴ └───────────┘ └─────┘ ┴
src └───────────┘ └───────────┘ └─────┘
typ ┴ └───────────┘ ┴ └───────────┘ └─────┘ ┴
doc └───────────┘ └───────────┘
362 t.induced subtype.val (λ x y, subtype.eq)
id ┴└──────┘ └─────────┘ ┴ ┴ └────────┘
src └──────┘ └─────────┘ └────────┘
typ ┴└──────┘ └─────────┘ ┴ ┴ └────────┘
doc └──────┘
363
364 /-- The extended distance on a subset of an emetric space is the restriction of
365 the original distance, by definition -/
366 theorem subtype.edist_eq {p : α → Prop} (x y : subtype p) : edist x y = edist x.1 y.1 := rfl
id ┴ └─────┘ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴┴ ┴┴ └─┘
src └─────┘ └───┘ ┴ └───┘ ┴ ┴ └─┘
typ ┴ └─────┘ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴┴ ┴┴ └─┘
367
368 /-- The product of two emetric spaces, with the max distance, is an extended
369 metric spaces. We make sure that the uniform structure thus constructed is the one
370 corresponding to the product of uniform spaces, to avoid diamond problems. -/
371 instance prod.emetric_space_max [emetric_space β] : emetric_space (α × β) :=
id └───────────┘ ┴ └───────────┘ ┴ ┴ ┴
src └───────────┘ └───────────┘ ┴
typ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴
doc └───────────┘ └───────────┘
372 { edist := λ x y, max (edist x.1 y.1) (edist x.2 y.2),
id ┴ ┴ └─┘ └───┘ ┴┴ ┴┴ └───┘ ┴┴ ┴┴
src └─┘ └───┘ ┴ ┴ └───┘ ┴ ┴
typ ┴ ┴ └─┘ └───┘ ┴┴ ┴┴ └───┘ ┴┴ ┴┴
373 edist_self := λ x, by simp,
id ┴
src └──┘
typ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
374 eq_of_edist_eq_zero := λ x y h, begin
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └─────
375 cases max_le_iff.1 (le_of_eq h) with h₁ h₂,
id └────────┘ └──────┘ ┴
src └────┘└────────┘└─┘ └──────┘┴ └──────────┘
typ └────┘└────────┘└─┘ └──────┘┴┴└──────────┘
doc └────┘ └─┘ ┴ └──────────┘
txt └────┘ └─┘ ┴ └──────────┘
par └────┘ └─┘ ┴ └──────────┘
pid ┴ └─┘ ┴ ┴└─────────┘
st ─────────────────────────────────────────────┘└─
376 have A : x.fst = y.fst := edist_le_zero.1 h₁,
id └───┘ ┴ └───┘ └───────────┘ └┘
src └───────┘└───┘┴┴┴└───┘└──┘└───────────┘└─┘
typ └───────┘└───┘┴┴┴└───┘└──┘└───────────┘└─┘└┘
doc └───────┘ ┴ ┴ └──┘ └─┘
txt └───────┘ ┴ ┴ └──┘ └─┘
par └───────┘ ┴ ┴ └──┘ └─┘
pid └────┘└─┘ ┴ ┴ └──┘ └─┘
st ───────────────────────────────────────────────┘└─
377 have B : x.snd = y.snd := edist_le_zero.1 h₂,
id └───┘ └───┘ └───────────┘ └┘
src └───────┘└───┘┴ ┴└───┘└──┘└───────────┘└─┘
typ └───────┘└───┘┴ ┴└───┘└──┘└───────────┘└─┘└┘
doc └───────┘ ┴ ┴ └──┘ └─┘
txt └───────┘ ┴ ┴ └──┘ └─┘
par └───────┘ ┴ ┴ └──┘ └─┘
pid └────┘└─┘ ┴ ┴ └──┘ └─┘
st ───────────────────────────────────────────────┘└─
378 exact prod.ext_iff.2 ⟨A, B⟩
id └──────────┘ ┴ ┴
src └────┘└──────────┘└─┘ └┘ └─
typ └────┘└──────────┘└─┘ ┴└┘┴└─
doc └────┘ └─┘ └┘ └─
txt └────┘ └─┘ └┘ └─
par └────┘ └─┘ └┘ └─
pid ┴ └─┘ └┘ ┴└
st ────────────────────────────────
379 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
380 edist_comm := λ x y, by simp [edist_comm],
id ┴ ┴ └────────┘
src └────┘└────────┘┴
typ ┴ ┴ └────┘└────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └────────────────┘
381 edist_triangle := λ x y z, max_le
id ┴ ┴ ┴ └────┘
src └────┘
typ ┴ ┴ ┴ └────┘
382 (le_trans (edist_triangle _ _ _) (add_le_add' (le_max_left _ _) (le_max_left _ _)))
id └──────┘ └────────────┘ └─────────┘ └─────────┘ └─────────┘
src └──────┘ └────────────┘ └─────────┘ └─────────┘ └─────────┘
typ └──────┘ └────────────┘ └─────────┘ └─────────┘ └─────────┘
383 (le_trans (edist_triangle _ _ _) (add_le_add' (le_max_right _ _) (le_max_right _ _))),
id └──────┘ └────────────┘ └─────────┘ └──────────┘ └──────────┘
src └──────┘ └────────────┘ └─────────┘ └──────────┘ └──────────┘
typ └──────┘ └────────────┘ └─────────┘ └──────────┘ └──────────┘
384 uniformity_edist := begin
st └─────
385 refine uniformity_prod.trans _,
id └───────────────────┘
src └─────┘└───────────────────┘└┘
typ └─────┘└───────────────────┘└┘
doc └─────┘ └┘
txt └─────┘ └┘
par └─────┘ └┘
pid ┴ └┘
st ─────────────────────────────────┘└─
386 simp [emetric_space.uniformity_edist, comap_infi],
id └────────────────────────────┘ └────────┘
src └────┘└────────────────────────────┘└┘└────────┘┴
typ └────┘└────────────────────────────┘└┘└────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ────────────────────────────────────────────────────┘└─
387 rw ← infi_inf_eq, congr, funext,
id └─────────┘
src └───┘└─────────┘ └───┘ └────┘
typ └───┘└─────────┘ └───┘ └────┘
doc └───┘ └────┘
txt └───┘ └───┘ └────┘
par └───┘ └───┘ └────┘
pid └─┘
st ───────────────────┘└─────┘└──────┘└─
388 rw ← infi_inf_eq, congr, funext,
id └─────────┘
src └───┘└─────────┘ └───┘ └────┘
typ └───┘└─────────┘ └───┘ └────┘
doc └───┘ └────┘
txt └───┘ └───┘ └────┘
par └───┘ └───┘ └────┘
pid └─┘
st ───────────────────┘└─────┘└──────┘└─
389 simp [inf_principal, ext_iff, max_lt_iff]
id └───────────┘ └─────┘ └────────┘
src └────┘└───────────┘└┘└─────┘└┘└────────┘└─
typ └────┘└───────────┘└┘└─────┘└┘└────────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st ──────────────────────────────────────────────
390 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
391 to_uniform_space := prod.uniform_space }
id └────────────────┘
src └────────────────┘
typ └────────────────┘
392
393 section pi
394 open finset
395 variables {π : β → Type*} [fintype β]
id └─────┘
src └─────┘
typ └─────┘
doc └─────┘
396
397 /-- The product of a finite number of emetric spaces, with the max distance, is still
398 an emetric space.
399 This construction would also work for infinite products, but it would not give rise
400 to the product topology. Hence, we only formalize it in the good situation of finitely many
401 spaces. -/
402 instance emetric_space_pi [∀b, emetric_space (π b)] : emetric_space (Πb, π b) :=
id ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └───────────┘ └───────────┘
typ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └───────────┘ └───────────┘
403 { edist := λ f g, finset.sup univ (λb, edist (f b) (g b)),
id ┴ ┴ └────────┘ └──┘ ┴ └───┘ ┴ ┴ ┴ ┴
src └────────┘ └──┘ └───┘
typ ┴ ┴ └────────┘ └──┘ ┴ └───┘ ┴ ┴ ┴ ┴
doc └────────┘ └──┘
404 edist_self := assume f, bot_unique $ finset.sup_le $ by simp,
id ┴ └────────┘ └───────────┘
src └────────┘ └───────────┘ └──┘
typ ┴ └────────┘ └───────────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
405 edist_comm := assume f g, by unfold edist; congr; funext a; exact edist_comm _ _,
id ┴ ┴ └────────┘
src └──────────┘ └───┘ └──────┘ └────┘└────────┘└──┘
typ ┴ ┴ └──────────┘ └───┘ └──────┘ └────┘└────────┘└──┘
doc └──────────┘ └──────┘ └────┘ └──┘
txt └──────────┘ └───┘ └──────┘ └────┘ └──┘
par └──────────┘ └───┘ └──────┘ └────┘ └──┘
pid └────┘ └┘ ┴ └──┘
st └──────────────────────────────────────────────────┘
406 edist_triangle := assume f g h,
id ┴ ┴ ┴
typ ┴ ┴ ┴
407 begin
st └─────
408 simp only [finset.sup_le_iff],
id └───────────────┘
src └─────────┘└───────────────┘┴
typ └─────────┘└───────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────────────┘└─
409 assume b hb,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────────┘└─
410 exact le_trans (edist_triangle _ (g b) _) (add_le_add' (le_sup hb) (le_sup hb))
id └──────┘ └────────────┘ ┴ ┴ └─────────┘ └────┘ └┘
src └────┘└──────┘┴ └────────────┘└─┘ ┴ └───┘ └─────────┘┴ ┴ └┘ └────┘┴ └──
typ └────┘└──────┘┴ └────────────┘└─┘ ┴┴┴└───┘ └─────────┘┴ ┴ └┘ └────┘┴└┘└──
doc └────┘ ┴ └─┘ ┴ └───┘ ┴ ┴ └┘ ┴ └──
txt └────┘ ┴ └─┘ ┴ └───┘ ┴ ┴ └┘ ┴ └──
par └────┘ ┴ └─┘ ┴ └───┘ ┴ ┴ └┘ ┴ └──
pid ┴ ┴ └─┘ ┴ └───┘ ┴ ┴ └┘ ┴ └┘└
st ──────────────────────────────────────────────────────────────────────────────────────
411 end,
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
412 eq_of_edist_eq_zero := assume f g eq0,
id ┴ ┴ └─┘
typ ┴ ┴ └─┘
413 begin
st └─────
414 have eq1 : sup univ (λ (b : β), edist (f b) (g b)) ≤ 0 := le_of_eq eq0,
id └─┘ └──┘ ┴ └───┘ ┴ ┴ ┴ └──────┘ └─┘
src └─────────┘└─┘┴└──┘┴ └────┘ └─┘└───┘┴ ┴ └┘ ┴ └─┘┴└────┘└──────┘┴
typ └─────────┘└─┘┴└──┘┴ └────┘┴└─┘└───┘┴ ┴┴ └┘ ┴┴ └─┘┴└────┘└──────┘┴└─┘
doc └─────────┘└─┘┴└──┘┴ └────┘ └─┘ ┴ ┴ └┘ ┴ └─┘ └────┘ ┴
txt └─────────┘ ┴ ┴ └────┘ └─┘ ┴ ┴ └┘ ┴ └─┘ └────┘ ┴
par └─────────┘ ┴ ┴ └────┘ └─┘ ┴ ┴ └┘ ┴ └─┘ └────┘ ┴
pid └──────┘└─┘ ┴ ┴ └────┘ └─┘ ┴ ┴ └┘ ┴ └─┘ ┴└───┘ ┴
st ───────────────────────────────────────────────────────────────────────────┘└─
415 simp only [finset.sup_le_iff] at eq1,
id └───────────────┘
src └─────────┘└───────────────┘└──────┘
typ └─────────┘└───────────────┘└──────┘
doc └─────────┘ └──────┘
txt └─────────┘ └──────┘
par └─────────┘ └──────┘
pid ┴└──┘└┘ ┴┴└────┘
st ─────────────────────────────────────────┘└─
416 exact (funext $ assume b, edist_le_zero.1 $ eq1 b $ mem_univ b),
id └────┘ └───────────┘ └─┘ └──────┘
src └────┘ └────┘┴ ┴ └──┘└───────────┘└─┘ ┴ ┴ ┴ ┴└──────┘┴ ┴
typ └────┘ └────┘┴ ┴ └──┘└───────────┘└─┘ ┴└─┘┴ ┴ ┴└──────┘┴ ┴
doc └────┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────┘└─
417 end,
st ──────┘
418 to_uniform_space := Pi.uniform_space _,
id └──────────────┘
src └──────────────┘
typ └──────────────┘
419 uniformity_edist := begin
st └─────
420 simp only [Pi.uniformity, emetric_space.uniformity_edist, comap_infi, gt_iff_lt, preimage_set_of_eq,
id └───────────┘ └────────────────────────────┘ └────────┘ └───────┘ └────────────────┘
src └─────────┘└───────────┘└┘└────────────────────────────┘└┘└────────┘└┘└───────┘└┘└────────────────┘└─
typ └─────────┘└───────────┘└┘└────────────────────────────┘└┘└────────┘└┘└───────┘└┘└────────────────┘└─
doc └─────────┘ └┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └─
st ─────────────────────────────────────────────────────────────────────────────────────────────────────────
421 comap_principal],
id └─────────────┘
src ─────────┘└─────────────┘┴
typ ─────────┘└─────────────┘┴
doc ─────────┘ ┴
txt ─────────┘ ┴
par ─────────┘ ┴
pid ─────────┘ ┴
st ─────────────────────────┘└─
422 rw infi_comm, congr, funext ε,
id └───────┘
src └─┘└───────┘ └───┘ └──────┘
typ └─┘└───────┘ └───┘ └──────┘
doc └─┘ └──────┘
txt └─┘ └───┘ └──────┘
par └─┘ └───┘ └──────┘
pid ┴ └┘
st ───────────────┘└─────┘└────────┘└─
423 rw infi_comm, congr, funext εpos,
id └───────┘
src └─┘└───────┘ └───┘ └─────────┘
typ └─┘└───────┘ └───┘ └─────────┘
doc └─┘ └─────────┘
txt └─┘ └───┘ └─────────┘
par └─┘ └───┘ └─────────┘
pid ┴ └───┘
st ───────────────┘└─────┘└───────────┘└─
424 change 0 < ε at εpos,
id ┴ ┴
src └───────┘┴┴ └──────┘
typ └───────┘┴┴┴└──────┘
doc └───────┘ ┴ └──────┘
txt └───────┘ ┴ └──────┘
par └───────┘ ┴ └──────┘
pid └─┘ ┴ ┴└─────┘
st ───────────────────────┘└─
425 simp [ext_iff, εpos]
id └─────┘ └──┘
src └────┘└─────┘└┘ └─
typ └────┘└─────┘└┘└──┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st ─────────────────────────
426 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
427
428 end pi
429
430 namespace emetric
431 variables {x y z : α} {ε ε₁ ε₂ : ennreal} {s : set α}
id └─────┘ └─┘
src └─────┘ └─┘
typ └─────┘ └─┘
doc └─────┘
432
433 /-- `emetric.ball x ε` is the set of all points `y` with `edist y x < ε` -/
434 def ball (x : α) (ε : ennreal) : set α := {y | edist y x < ε}
id ┴ └─────┘ └─┘ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴
src └─────┘ └─┘ ┴ └───┘ ┴
typ ┴ └─────┘ └─┘ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴
doc └─────┘
435
436 @[simp] theorem mem_ball : y ∈ ball x ε ↔ edist y x < ε := iff.rfl
id ┴ ┴ └──┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └─────┘
src ┴ └──┘ ┴ └───┘ ┴ └─────┘
typ ┴ ┴ └──┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └─────┘
doc └──┘ └──┘
437
438 theorem mem_ball' : y ∈ ball x ε ↔ edist x y < ε := by rw edist_comm; refl
id ┴ ┴ └──┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └────────┘
src ┴ └──┘ ┴ └───┘ ┴ └─┘└────────┘ └────
typ ┴ ┴ └──┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └─┘└────────┘ └────
doc └──┘ └─┘ └────
txt └─┘ └────
par └─┘ └────
pid ┴ └
st └────────────────────
439
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
440 /-- `emetric.closed_ball x ε` is the set of all points `y` with `edist y x ≤ ε` -/
441 def closed_ball (x : α) (ε : ennreal) := {y | edist y x ≤ ε}
id ┴ └─────┘ ┴┴ └───┘ ┴ ┴ ┴ ┴
src └─────┘ ┴ └───┘ ┴
typ ┴ └─────┘ ┴┴ └───┘ ┴ ┴ ┴ ┴
doc └─────┘
442
443 @[simp] theorem mem_closed_ball : y ∈ closed_ball x ε ↔ edist y x ≤ ε := iff.rfl
id ┴ ┴ └─────────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └─────┘
src ┴ └─────────┘ ┴ └───┘ ┴ └─────┘
typ ┴ ┴ └─────────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └─────┘
doc └──┘ └─────────┘
444
445 theorem ball_subset_closed_ball : ball x ε ⊆ closed_ball x ε :=
id └──┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
src └──┘ ┴ └─────────┘
typ └──┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
doc └──┘ └─────────┘
446 assume y, by simp; intros h; apply le_of_lt h
id ┴ └──────┘ ┴
src └──┘ └──────┘ └────┘└──────┘┴ └
typ ┴ └──┘ └──────┘ └────┘└──────┘┴┴└
doc └──┘ └──────┘ └────┘ ┴ └
txt └──┘ └──────┘ └────┘ ┴ └
par └──┘ └──────┘ └────┘ ┴ └
pid └┘ ┴ ┴ └
st └─────────────────────────────────
447
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
448 theorem pos_of_mem_ball (hy : y ∈ ball x ε) : 0 < ε :=
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘
449 lt_of_le_of_lt (zero_le _) hy
id └────────────┘ └─────┘ └┘
src └────────────┘ └─────┘
typ └────────────┘ └─────┘ └┘
450
451 theorem mem_ball_self (h : 0 < ε) : x ∈ ball x ε :=
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc └──┘
452 show edist x x < ε, by rw edist_self; assumption
id └───┘ ┴ ┴ ┴ ┴ └────────┘
src └───┘ ┴ └─┘└────────┘ └──────────
typ └───┘ ┴ ┴ ┴ ┴ └─┘└────────┘ └──────────
doc └─┘ └──────────
txt └─┘ └──────────
par └─┘ └──────────
pid ┴ └
st └──────────────────────────
453
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
454 theorem mem_closed_ball_self : x ∈ closed_ball x ε :=
id ┴ ┴ └─────────┘ ┴ ┴
src ┴ └─────────┘
typ ┴ ┴ └─────────┘ ┴ ┴
doc └─────────┘
455 show edist x x ≤ ε, by rw edist_self; exact bot_le
id └───┘ ┴ ┴ ┴ ┴ └────────┘ └────┘
src └───┘ ┴ └─┘└────────┘ └────┘└────┘└
typ └───┘ ┴ ┴ ┴ ┴ └─┘└────────┘ └────┘└────┘└
doc └─┘ └────┘ └
txt └─┘ └────┘ └
par └─┘ └────┘ └
pid ┴ ┴ └
st └────────────────────────────
456
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
457 theorem mem_ball_comm : x ∈ ball y ε ↔ y ∈ ball x ε :=
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src ┴ └──┘ ┴ ┴ └──┘
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc └──┘ └──┘
458 by simp [edist_comm]
id └────────┘
src └────┘└────────┘└─
typ └────┘└────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └──────────────────
459
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
460 theorem ball_subset_ball (h : ε₁ ≤ ε₂) : ball x ε₁ ⊆ ball x ε₂ :=
id └┘ ┴ └┘ └──┘ ┴ └┘ ┴ └──┘ ┴ └┘
src ┴ └──┘ ┴ └──┘
typ └┘ ┴ └┘ └──┘ ┴ └┘ ┴ └──┘ ┴ └┘
doc └──┘ └──┘
461 λ y (yx : _ < ε₁), lt_of_lt_of_le yx h
id ┴ ┴ └┘ └────────────┘ └┘ ┴
src ┴ └────────────┘
typ ┴ ┴ └┘ └────────────┘ └┘ ┴
462
463 theorem closed_ball_subset_closed_ball (h : ε₁ ≤ ε₂) :
id └┘ ┴ └┘
src ┴
typ └┘ ┴ └┘
464 closed_ball x ε₁ ⊆ closed_ball x ε₂ :=
id └─────────┘ ┴ └┘ ┴ └─────────┘ ┴ └┘
src └─────────┘ ┴ └─────────┘
typ └─────────┘ ┴ └┘ ┴ └─────────┘ ┴ └┘
doc └─────────┘ └─────────┘
465 λ y (yx : _ ≤ ε₁), le_trans yx h
id ┴ ┴ └┘ └──────┘ └┘ ┴
src ┴ └──────┘
typ ┴ ┴ └┘ └──────┘ └┘ ┴
466
467 theorem ball_disjoint (h : ε₁ + ε₂ ≤ edist x y) : ball x ε₁ ∩ ball y ε₂ = ∅ :=
id └┘ ┴ └┘ ┴ └───┘ ┴ ┴ └──┘ ┴ └┘ ┴ └──┘ ┴ └┘ ┴ ┴
src ┴ ┴ └───┘ └──┘ ┴ └──┘ ┴ ┴
typ └┘ ┴ └┘ ┴ └───┘ ┴ ┴ └──┘ ┴ └┘ ┴ └──┘ ┴ └┘ ┴ ┴
doc └──┘ └──┘
468 eq_empty_iff_forall_not_mem.2 $ λ z ⟨h₁, h₂⟩,
id └─────────────────────────┘┴ ┴ ┴└┘ └┘
src └─────────────────────────┘┴
typ └─────────────────────────┘┴ ┴ ┴└┘ └┘
469 not_lt_of_le (edist_triangle_left x y z)
id └──────────┘ └─────────────────┘ ┴ ┴ ┴
src └──────────┘ └─────────────────┘
typ └──────────┘ └─────────────────┘ ┴ ┴ ┴
doc └─────────────────┘
470 (lt_of_lt_of_le (ennreal.add_lt_add h₁ h₂) h)
id └────────────┘ └────────────────┘ ┴
src └────────────┘ └────────────────┘
typ └────────────┘ └────────────────┘ ┴
471
472 theorem ball_subset (h : edist x y + ε₁ ≤ ε₂) (h' : edist x y < ⊤) : ball x ε₁ ⊆ ball y ε₂ :=
id └───┘ ┴ ┴ ┴ └┘ ┴ └┘ └───┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ └──┘ ┴ └┘
src └───┘ ┴ ┴ └───┘ ┴ ┴ └──┘ ┴ └──┘
typ └───┘ ┴ ┴ ┴ └┘ ┴ └┘ └───┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ └──┘ ┴ └┘
doc └──┘ └──┘
473 λ z zx, calc
id ┴ └┘
typ ┴ └┘
474 edist z y ≤ edist z x + edist x y : edist_triangle _ _ _
id └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └────────────┘
src └───┘ └───┘ ┴ └───┘ └────────────┘
typ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └────────────┘
475 ... = edist x y + edist z x : add_comm _ _
id └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └──────┘
src └───┘ ┴ └───┘ └──────┘
typ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └──────┘
476 ... < edist x y + ε₁ : (ennreal.add_lt_add_iff_left h').2 zx
id └───┘ ┴ ┴ ┴ └┘ └─────────────────────────┘ └┘ ┴ └┘
src └───┘ ┴ └─────────────────────────┘ ┴
typ └───┘ ┴ ┴ ┴ └┘ └─────────────────────────┘ └┘ ┴ └┘
477 ... ≤ ε₂ : h
id └┘ ┴
typ └┘ ┴
478
479 theorem exists_ball_subset_ball (h : y ∈ ball x ε) : ∃ ε' > 0, ball y ε' ⊆ ball x ε :=
id ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ └┘ ┴ └──┘ ┴ ┴
src ┴ └──┘ ┴ ┴ └──┘ ┴ └──┘
typ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ └┘ ┴ └──┘ ┴ ┴
doc └──┘ └──┘ └──┘
480 begin
st └─────
481 have : 0 < ε - edist y x := by simpa using h,
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴
src └───────┘┴┴ ┴┴┴└───┘┴ ┴ └──┘ ┴└──────────┘
typ └───────┘┴┴┴┴┴┴└───┘┴┴┴┴└──┘ ┴└──────────┘┴
doc └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└──────────┘
txt └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└──────────┘
par └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└──────────┘
pid └───┘└──┘ ┴ ┴ ┴ ┴ ┴ └──┘ └───────────┘
st ───────────────────────────────┘└────────────┘└─
482 refine ⟨ε - edist y x, this, ball_subset _ _⟩,
id ┴ └───┘ ┴ ┴ └──┘ └─────────┘
src └─────┘ ┴ ┴└───┘┴ ┴ └┘ └┘└─────────┘└───┘
typ └─────┘ ┴┴ ┴└───┘┴┴┴┴└┘└──┘└┘└─────────┘└───┘
doc └─────┘ ┴ ┴ ┴ ┴ └┘ └┘ └───┘
txt └─────┘ ┴ ┴ ┴ ┴ └┘ └┘ └───┘
par └─────┘ ┴ ┴ ┴ ┴ └┘ └┘ └───┘
pid ┴ ┴ ┴ ┴ ┴ └┘ └┘ └───┘
st ──────────────────────────────────────────────┘└─
483 { rw ennreal.add_sub_cancel_of_le (le_of_lt h), apply le_refl _},
id └──────────────────────────┘ └──────┘ ┴ └─────┘
src └─┘└──────────────────────────┘┴ └──────┘┴ ┴ └────┘└─────┘└┘
typ └─┘└──────────────────────────┘┴ └──────┘┴┴┴ └────┘└─────┘└┘
doc └─┘ ┴ ┴ ┴ └────┘ └┘
txt └─┘ ┴ ┴ ┴ └────┘ └┘
par └─┘ ┴ ┴ ┴ └────┘ └┘
pid ┴ ┴ ┴ ┴ ┴ └┘
st ───┘└──────────────────────────────────────────┘└───────────────┘└┘└
484 { have : edist y x ≠ ⊤ := lattice.ne_top_of_lt h, apply lt_top_iff_ne_top.2 this }
id └───┘ ┴ ┴ ┴ ┴ └──────────────────┘ ┴ └───────────────┘ └──┘
src └─────┘└───┘┴ ┴ ┴┴┴┴└──┘└──────────────────┘┴ └────┘└───────────────┘└─┘ ┴
typ └─────┘└───┘┴┴┴┴┴┴┴┴└──┘└──────────────────┘┴┴ └────┘└───────────────┘└─┘└──┘┴
doc └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └────┘ └─┘ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └────┘ └─┘ ┴
par └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └────┘ └─┘ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴
st ─────────────────────────────────────────────────┘└───────────────────────────────┘└─
485 end
st ──┘
486
487 theorem ball_eq_empty_iff : ball x ε = ∅ ↔ ε = 0 :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
488 eq_empty_iff_forall_not_mem.trans
id └─────────────────────────┘└────┘
src └─────────────────────────┘└────┘
typ └─────────────────────────┘└────┘
489 ⟨λh, le_bot_iff.1 (le_of_not_gt (λ ε0, h _ (mem_ball_self ε0))),
id ┴ └────────┘┴ └──────────┘ └┘ ┴ └───────────┘ └┘
src └────────┘┴ └──────────┘ └───────────┘
typ ┴ └────────┘┴ └──────────┘ └┘ ┴ └───────────┘ └┘
490 λε0 y h, not_lt_of_le (le_of_eq ε0) (pos_of_mem_ball h)⟩
id └┘ ┴ ┴ └──────────┘ └──────┘ └┘ └─────────────┘ ┴
src └──────────┘ └──────┘ └─────────────┘
typ └┘ ┴ ┴ └──────────┘ └──────┘ └┘ └─────────────┘ ┴
491
492 theorem nhds_eq : 𝓝 x = (⨅ε:{ε:ennreal // ε>0}, principal (ball x ε.val)) :=
id ┴ ┴ ┴ ┴ ┴ └─────┘ ┴┴ ┴ └───────┘ └──┘ ┴ ┴└──┘
src ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └───────┘ └──┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴┴ ┴ └───────┘ └──┘ ┴ ┴└──┘
doc ┴ ┴ └─────┘ ┴ └───────┘ └──┘
493 begin
st └─────
494 rw [nhds_eq_uniformity, uniformity_edist'', lift'_infi],
id └────────────────┘ └────────────────┘ └────────┘
src └──┘└────────────────┘└┘└────────────────┘└┘└────────┘┴
typ └──┘└────────────────┘└┘└────────────────┘└┘└────────┘┴
doc └──┘ └┘└────────────────┘└┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ───────────────────────┘└──────────────────┘└──────────┘└──
495 { apply congr_arg, funext ε,
id └───────┘
src └────┘└───────┘ └──────┘
typ └────┘└───────┘ └──────┘
doc └────┘ └──────┘
txt └────┘ └──────┘
par └────┘ └──────┘
pid ┴ └┘
st ───┘└─────────────┘└────────┘└─
496 rw [lift'_principal],
id └─────────────┘
src └──┘└─────────────┘┴
typ └──┘└─────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ──────────────────────┘└──
497 { simp [ball, edist_comm] },
id └──┘ └────────┘
src └────┘└──┘└┘└────────┘└┘
typ └────┘└──┘└┘└────────┘└┘
doc └────┘└──┘└┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ─────┘└──────────────────────┘└┘└
498 { exact monotone_preimage } },
id └───────────────┘
src └────┘└───────────────┘┴
typ └────┘└───────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────────┘└──┘└
499 { exact ⟨⟨1, ennreal.zero_lt_one⟩⟩ },
id └─────────────────┘
src └────┘ └─┘└─────────────────┘└─┘
typ └────┘ └─┘└─────────────────┘└─┘
doc └────┘ └─┘ └─┘
txt └────┘ └─┘ └─┘
par └────┘ └─┘ └─┘
pid ┴ └─┘ └┘┴
st ───┘└───────────────────────────────┘└┘└
500 { intros, refl }
src └────┘ └───┘
typ └────┘ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴
st ─────────┘└─────┘└─
501 end
st ──┘
502
503 theorem mem_nhds_iff : s ∈ 𝓝 x ↔ ∃ε>0, ball x ε ⊆ s :=
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └──┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc ┴ └──┘
504 begin
st └─────
505 rw [nhds_eq, mem_infi],
id └─────┘ └──────┘
src └──┘└─────┘└┘└──────┘┴
typ └──┘└─────┘└┘└──────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────┘└────────┘└──
506 { simp },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ───┘└───┘└┘└
507 { intros y z, cases y with y hy, cases z with z hz,
id ┴ ┴
src └────────┘ └────┘ └────────┘ └────┘ └────────┘
typ └────────┘ └────┘┴└────────┘ └────┘┴└────────┘
doc └────────┘ └────┘ └────────┘ └────┘ └────────┘
txt └────────┘ └────┘ └────────┘ └────┘ └────────┘
par └────────┘ └────┘ └────────┘ └────┘ └────────┘
pid └──┘ ┴ └────────┘ ┴ └────────┘
st ───┘└────────┘└─────────────────┘└─────────────────┘└─
508 refine ⟨⟨min y z, lt_min hy hz⟩, _⟩,
id └─┘ ┴ ┴ └────┘ └┘ └┘
src └─────┘ └─┘┴ ┴ └┘└────┘┴ ┴ └───┘
typ └─────┘ └─┘┴┴┴┴└┘└────┘┴└┘┴└┘└───┘
doc └─────┘ ┴ ┴ └┘ ┴ ┴ └───┘
txt └─────┘ ┴ ┴ └┘ ┴ ┴ └───┘
par └─────┘ ┴ ┴ └┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ └┘ ┴ ┴ └───┘
st ──────────────────────────────────────┘└─
509 simp [ball_subset_ball, min_le_left, min_le_right, (≥)] },
id └──────────────┘ └─────────┘ └──────────┘ ┴
src └────┘└──────────────┘└┘└─────────┘└┘└──────────┘└┘┴└──┘
typ └────┘└──────────────┘└┘└─────────┘└┘└──────────┘└┘┴└──┘
doc └────┘ └┘ └┘ └┘ └──┘
txt └────┘ └┘ └┘ └┘ └──┘
par └────┘ └┘ └┘ └┘ └──┘
pid ┴┴ └┘ └┘ └┘ └─┘┴
st ───────────────────────────────────────────────────────────┘└┘└
510 { exact ⟨⟨1, ennreal.zero_lt_one⟩⟩ }
id └─────────────────┘
src └────┘ └─┘└─────────────────┘└─┘
typ └────┘ └─┘└─────────────────┘└─┘
doc └────┘ └─┘ └─┘
txt └────┘ └─┘ └─┘
par └────┘ └─┘ └─┘
pid ┴ └─┘ └┘┴
st ────────────────────────────────────┘└─
511 end
st ──┘
512
513 theorem is_open_iff : is_open s ↔ ∀x∈s, ∃ε>0, ball x ε ⊆ s :=
id └─────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ └──┘ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └─────┘ └──┘
514 by simp [is_open_iff_nhds, mem_nhds_iff]
id └──────────────┘ └──────────┘
src └────┘└──────────────┘└┘└──────────┘└─
typ └────┘└──────────────┘└┘└──────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └──────────────────────────────────────
515
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
516 theorem is_open_ball : is_open (ball x ε) :=
id └─────┘ └──┘ ┴ ┴
src └─────┘ └──┘
typ └─────┘ └──┘ ┴ ┴
doc └─────┘ └──┘
517 is_open_iff.2 $ λ y, exists_ball_subset_ball
id └─────────┘┴ ┴ └─────────────────────┘
src └─────────┘┴ └─────────────────────┘
typ └─────────┘┴ ┴ └─────────────────────┘
518
519 theorem ball_mem_nhds (x : α) {ε : ennreal} (ε0 : 0 < ε) : ball x ε ∈ 𝓝 x :=
id ┴ └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ └──┘ ┴ ┴
typ ┴ └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └──┘ ┴
520 mem_nhds_sets is_open_ball (mem_ball_self ε0)
id └───────────┘ └──────────┘ └───────────┘ └┘
src └───────────┘ └──────────┘ └───────────┘
typ └───────────┘ └──────────┘ └───────────┘ └┘
521
522 /-- ε-characterization of the closure in emetric spaces -/
523 theorem mem_closure_iff' :
524 x ∈ closure s ↔ ∀ε>0, ∃y ∈ s, edist x y < ε :=
id ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴┴ └───┘ ┴ ┴ ┴ ┴
src ┴ └─────┘ ┴ ┴ ┴ └───┘ ┴
typ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴┴ └───┘ ┴ ┴ ┴ ┴
doc └─────┘
525 ⟨begin
st └─────
526 intros hx ε hε,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───────────────┘└─
527 obtain ⟨y, hy⟩ : (ball x ε ∩ s).nonempty,
id └──┘ ┴ ┴ ┴ ┴
src └───────────────┘ └──┘┴ ┴ ┴┴┴ └────────┘
typ └───────────────┘ └──┘┴┴┴┴┴┴┴┴└────────┘
doc └───────────────┘ └──┘┴ ┴ ┴ ┴ └────────┘
txt └───────────────┘ ┴ ┴ ┴ ┴ └────────┘
par └───────────────┘ ┴ ┴ ┴ ┴ └────────┘
pid └─────────┘ ┴ ┴ ┴ ┴ └───────┘┴
st ─────────────────────────────────────────┘└─
528 from mem_closure_iff.1 hx _ is_open_ball (mem_ball_self hε),
id └─────────────┘ └┘ └──────────┘ └───────────┘ └┘
src └───┘└─────────────┘└─┘ └─┘└──────────┘┴ └───────────┘┴ ┴
typ └───┘└─────────────┘└─┘└┘└─┘└──────────┘┴ └───────────┘┴└┘┴
doc └───┘ └─┘ └─┘ ┴ ┴ ┴
txt └───┘ └─┘ └─┘ ┴ ┴ ┴
par └───┘ └─┘ └─┘ ┴ ┴ ┴
pid └───┘ └─┘ └─┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────┘└─
529 simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ─────┘└─
530 exact ⟨y, ⟨hy.2, by have B := hy.1; simpa [mem_ball'] using B⟩⟩
id ┴ └┘ └┘ └───────┘ ┴
src └────┘ └┘ └──┘ ┴└────────┘ └┘└┘└─────┘└───────┘└──────┘ └─┘
typ └────┘ ┴└┘ └┘└──┘ ┴└────────┘└┘└┘└┘└─────┘└───────┘└──────┘┴└─┘
doc └────┘ └┘ └──┘ ┴└────────┘ └┘└┘└─────┘ └──────┘ └─┘
txt └────┘ └┘ └──┘ ┴└────────┘ └┘└┘└─────┘ └──────┘ └─┘
par └────┘ └┘ └──┘ ┴└────────┘ └┘└┘└─────┘ └──────┘ └─┘
pid ┴ └┘ └──┘ └─────────┘ └─────────┘ └──────┘ └┘┴
st ────────────────────┘└────────────────────────────────────────┘└─┘
531 end,
st └─┘
532 begin
st └─────
533 intros H,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ─────────┘└─
534 apply mem_closure_iff.2,
id └─────────────┘
src └────┘└─────────────┘└┘
typ └────┘└─────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ────────────────────────┘└─
535 intros o ho xo,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───────────────┘└─
536 rcases is_open_iff.1 ho x xo with ⟨ε, ⟨εpos, hε⟩⟩,
id └─────────┘ └┘ ┴ └┘
src └─────┘└─────────┘└─┘ ┴ ┴ └───────────────────┘
typ └─────┘└─────────┘└─┘└┘┴┴┴└┘└───────────────────┘
doc └─────┘ └─┘ ┴ ┴ └───────────────────┘
txt └─────┘ └─┘ ┴ ┴ └───────────────────┘
par └─────┘ └─┘ ┴ ┴ └───────────────────┘
pid ┴ └─┘ ┴ ┴ └───────────────────┘
st ──────────────────────────────────────────────────┘└─
537 rcases H ε εpos with ⟨y, ⟨ys, ydist⟩⟩,
id ┴ ┴ └──┘
src └─────┘ ┴ ┴ └────────────────────┘
typ └─────┘┴┴┴┴└──┘└────────────────────┘
doc └─────┘ ┴ ┴ └────────────────────┘
txt └─────┘ ┴ ┴ └────────────────────┘
par └─────┘ ┴ ┴ └────────────────────┘
pid ┴ ┴ ┴ └────────────────────┘
st ──────────────────────────────────────┘└─
538 have B : y ∈ o ∩ s := ⟨hε (by simpa [edist_comm]), ys⟩,
id ┴ ┴ ┴ ┴ └┘ └────────┘ └┘
src └───────┘ ┴┴┴ ┴ ┴ └──┘ ┴ ┴└─────┘└────────┘┴└─┘ ┴
typ └───────┘┴┴┴┴┴┴ ┴┴└──┘ └┘┴ ┴└─────┘└────────┘┴└─┘└┘┴
doc └───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴└─────┘ ┴└─┘ ┴
txt └───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴└─────┘ ┴└─┘ ┴
par └───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴└─────┘ ┴└─┘ ┴
pid └────┘└─┘ ┴ ┴ ┴ ┴ └──┘ ┴ └──────┘ └──┘ ┴
st ──────────────────────────────┘└─────────────────┘└────┘└─
539 exact ⟨y, B⟩
id ┴ ┴
src └────┘ └┘ └┘
typ └────┘ ┴└┘┴└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴ └┘ ┴┴
st ──────────────┘
540 end⟩
st └─┘
541
542 theorem tendsto_nhds {f : filter β} {u : β → α} {a : α} :
id └────┘ ┴ ┴ ┴ ┴
src └────┘
typ └────┘ ┴ ┴ ┴ ┴
543 tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∃ n ∈ f, ∀x ∈ n, edist (u x) a < ε :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴
544 ⟨λ H ε ε0, ⟨u⁻¹' (ball a ε), H (ball_mem_nhds _ ε0), by simp⟩,
id ┴ ┴ └┘ ┴└─┘ └──┘ ┴ ┴ ┴ └───────────┘ └┘
src └─┘ └──┘ └───────────┘ └──┘
typ ┴ ┴ └┘ ┴└─┘ └──┘ ┴ ┴ ┴ └───────────┘ └┘ └──┘
doc └─┘ └──┘ └──┘
txt └──┘
par └──┘
st └───┘
545 λ H s hs,
id ┴ ┴ └┘
typ ┴ ┴ └┘
546 let ⟨ε, ε0, hε⟩ := mem_nhds_iff.1 hs, ⟨δ, δ0, hδ⟩ := H _ ε0 in
id └─┘ └┘ └┘ └──────────┘┴ └┘ └┘ └┘ ┴
src └──────────┘┴
typ └─┘ └┘ └┘ └──────────┘┴ └┘ └┘ └┘ ┴
547 f.sets_of_superset δ0 (λx xδ, hε (hδ x xδ))⟩
id ┴└───────────────┘ ┴ └┘ ┴ └┘
src └───────────────┘
typ ┴└───────────────┘ ┴ └┘ ┴ └┘
548
549 theorem tendsto_at_top [inhabited β] [semilattice_sup β] (u : β → α) {a : α} :
id └───────┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴
src └───────┘ └─────────────┘
typ └───────┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴
doc └─────────────┘
550 tendsto u at_top (𝓝 a) ↔ ∀ε>0, ∃N, ∀n≥N, edist (u n) a < ε :=
id └─────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
typ └─────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └────┘ ┴
551 begin
st └─────
552 rw tendsto_nhds,
id └──────────┘
src └─┘└──────────┘
typ └─┘└──────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────┘└─
553 apply forall_congr,
id └──────────┘
src └────┘└──────────┘
typ └────┘└──────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
554 intro ε,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ────────┘└─
555 apply forall_congr,
id └──────────┘
src └────┘└──────────┘
typ └────┘└──────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
556 intro hε,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └─┘
st ─────────┘└─
557 simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ─────┘└─
558 exact ⟨λ ⟨s, ⟨N, hN⟩, hs⟩, ⟨N, λn hn, hs _ (hN _ hn)⟩, λ ⟨N, hN⟩, ⟨{n | n ≥ N}, ⟨⟨N, by simp⟩, hN⟩⟩⟩,
id ┴ └┘ └┘ ┴ └┘ ┴ ┴
src └────┘ └┘ └┘ └┘ └─┘ └─┘ └┘ └────┘ └─┘ └─┘ └──┘ └┘ └┘ └─┘ ┴└──┘ ┴┴┴ └─┘ └┘ ┴└──┘└─┘ └─┘
typ └────┘ └┘ └┘ ┴└┘└┘└─┘└┘└─┘ └┘ └────┘ └─┘ └─┘ └──┘ └┘┴└┘└┘└─┘ ┴└──┘ ┴┴┴ └─┘ └┘ ┴└──┘└─┘ └─┘
doc └────┘ └┘ └┘ └┘ └─┘ └─┘ └┘ └────┘ └─┘ └─┘ └──┘ └┘ └┘ └─┘ └──┘ ┴ ┴ └─┘ └┘ ┴└──┘└─┘ └─┘
txt └────┘ └┘ └┘ └┘ └─┘ └─┘ └┘ └────┘ └─┘ └─┘ └──┘ └┘ └┘ └─┘ └──┘ ┴ ┴ └─┘ └┘ ┴└──┘└─┘ └─┘
par └────┘ └┘ └┘ └┘ └─┘ └─┘ └┘ └────┘ └─┘ └─┘ └──┘ └┘ └┘ └─┘ └──┘ ┴ ┴ └─┘ └┘ ┴└──┘└─┘ └─┘
pid ┴ └┘ └┘ └┘ └─┘ └─┘ └┘ └────┘ └─┘ └─┘ └──┘ └┘ └┘ └─┘ └──┘ ┴ ┴ └─┘ └┘ └──────┘ └─┘
st ────────────────────────────────────────────────────────────────────────────────────────┘└───┘└──────┘└─
559 end
st ──┘
560
561 /-- In an emetric space, Cauchy sequences are characterized by the fact that, eventually,
562 the edistance between its elements is arbitrarily small -/
563 theorem cauchy_seq_iff [inhabited β] [semilattice_sup β] {u : β → α} :
id └───────┘ ┴ └─────────────┘ ┴ ┴ ┴
src └───────┘ └─────────────┘
typ └───────┘ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘
564 cauchy_seq u ↔ ∀ε>0, ∃N, ∀m n≥N, edist (u n) (u m) < ε :=
id └────────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ ┴ └───┘ ┴
typ └────────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘
565 begin
st └─────
566 simp only [cauchy_seq, emetric.cauchy_iff, true_and, exists_prop, filter.mem_at_top_sets,
id └────────┘ └────────────────┘ └──────┘ └─────────┘ └────────────────────┘
src └─────────┘└────────┘└┘└────────────────┘└┘└──────┘└┘└─────────┘└┘└────────────────────┘└─
typ └─────────┘└────────┘└┘└────────────────┘└┘└──────┘└┘└─────────┘└┘└────────────────────┘└─
doc └─────────┘└────────┘└┘└────────────────┘└┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └─
st ────────────────────────────────────────────────────────────────────────────────────────────
567 filter.at_top_ne_bot, filter.mem_map, ne.def, filter.map_eq_bot_iff, not_false_iff, set.mem_set_of_eq],
id └──────────────────┘ └────────────┘ └────┘ └───────────────────┘ └───────────┘ └───────────────┘
src ───┘└──────────────────┘└┘└────────────┘└┘└────┘└┘└───────────────────┘└┘└───────────┘└┘└───────────────┘┴
typ ───┘└──────────────────┘└┘└────────────┘└┘└────┘└┘└───────────────────┘└┘└───────────┘└┘└───────────────┘┴
doc ───┘ └┘ └┘ └┘ └┘ └┘ ┴
txt ───┘ └┘ └┘ └┘ └┘ └┘ ┴
par ───┘ └┘ └┘ └┘ └┘ └┘ ┴
pid ───┘ └┘ └┘ └┘ └┘ └┘ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
568 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
569 { intros H ε εpos,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ───┘└─────────────┘└─
570 rcases H ε εpos with ⟨t, ⟨N, hN⟩, ht⟩,
id ┴ ┴ └──┘
src └─────┘ ┴ ┴ └────────────────────┘
typ └─────┘┴┴┴┴└──┘└────────────────────┘
doc └─────┘ ┴ ┴ └────────────────────┘
txt └─────┘ ┴ ┴ └────────────────────┘
par └─────┘ ┴ ┴ └────────────────────┘
pid ┴ ┴ ┴ └────────────────────┘
st ────────────────────────────────────────┘└─
571 exact ⟨N, λm n hm hn, ht _ _ (hN _ hn) (hN _ hm)⟩ },
id ┴ └┘ └┘
src └────┘ └┘ └─────────┘ └───┘ └─┘ └┘ └─┘ └─┘
typ └────┘ ┴└┘ └─────────┘└┘└───┘ └─┘ └┘ └┘└─┘ └─┘
doc └────┘ └┘ └─────────┘ └───┘ └─┘ └┘ └─┘ └─┘
txt └────┘ └┘ └─────────┘ └───┘ └─┘ └┘ └─┘ └─┘
par └────┘ └┘ └─────────┘ └───┘ └─┘ └┘ └─┘ └─┘
pid ┴ └┘ └─────────┘ └───┘ └─┘ └┘ └─┘ └┘┴
st ─────────────────────────────────────────────────────┘└┘└
572 { intros H ε εpos,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ──────────────────┘└─
573 rcases H (ε/2) (ennreal.half_pos εpos) with ⟨N, hN⟩,
id ┴ ┴┴ └──────────────┘ └──┘
src └─────┘ ┴ ┴└─┘ └──────────────┘┴ └────────────┘
typ └─────┘┴┴ ┴┴└─┘ └──────────────┘┴└──┘└────────────┘
doc └─────┘ ┴ └─┘ ┴ └────────────┘
txt └─────┘ ┴ └─┘ ┴ └────────────┘
par └─────┘ ┴ └─┘ ┴ └────────────┘
pid ┴ ┴ └─┘ ┴ └────────────┘
st ──────────────────────────────────────────────────────┘└─
574 existsi ball (u N) (ε/2),
id └──┘ ┴ ┴ ┴
src └──────┘└──┘┴ ┴ └┘ └┘
typ └──────┘└──┘┴ ┴┴┴└┘ ┴ └┘
doc └──────┘└──┘┴ ┴ └┘ └┘
txt └──────┘ ┴ ┴ └┘ └┘
par └──────┘ ┴ ┴ └┘ └┘
pid ┴ ┴ ┴ └┘ └┘
st ───────────────────────────┘└─
575 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
576 { exact ⟨N, λx hx, hN _ _ (le_refl N) hx⟩ },
id └┘ └─────┘ ┴
src └────┘ └┘ └────┘ └───┘ └─────┘┴ └┘ └┘
typ └────┘ └┘ └────┘└┘└───┘ └─────┘┴┴└┘ └┘
doc └────┘ └┘ └────┘ └───┘ ┴ └┘ └┘
txt └────┘ └┘ └────┘ └───┘ ┴ └┘ └┘
par └────┘ └┘ └────┘ └───┘ ┴ └┘ └┘
pid ┴ └┘ └────┘ └───┘ ┴ └┘ ┴┴
st ─────┘└──────────────────────────────────────┘└┘└
577 { exact λx y hx hy, calc
src └────┘ └─────────┘ └
typ └────┘ └─────────┘ └
doc └────┘ └─────────┘ └
txt └────┘ └─────────┘ └
par └────┘ └─────────┘ └
pid ┴ └─────────┘ └
st ─────────────────────────────
578 edist x y ≤ edist x (u N) + edist y (u N) : edist_triangle_right _ _ _
id └───┘ ┴ ┴ └──────────────────┘
src ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴└───┘┴ ┴ ┴ └──┘└──────────────────┘└──────
typ ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴└───┘┴ ┴ ┴┴┴└──┘└──────────────────┘└──────
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └──────
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └──────
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └──────
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └──────
st ───────────────────────────────────────────────────────────────────────────────
579 ... < ε/2 + ε/2 : ennreal.add_lt_add hx hy
id ┴ └────────────────┘
src ───────────┘ ┴ └┘┴┴ └──┘└────────────────┘┴ ┴ └
typ ───────────┘ ┴ └┘┴┴ └──┘└────────────────┘┴ ┴ └
doc ───────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
txt ───────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
par ───────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
pid ───────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
st ───────────────────────────────────────────────────
580 ... = ε : ennreal.add_halves _ } }
id ┴ └────────────────┘
src ───────────┘ ┴ └─┘└────────────────┘└─┘
typ ───────────┘ ┴┴└─┘└────────────────┘└─┘
doc ───────────┘ ┴ └─┘ └─┘
txt ───────────┘ ┴ └─┘ └─┘
par ───────────┘ ┴ └─┘ └─┘
pid ───────────┘ ┴ └─┘ └┘┴
st ──────────────────────────────────────┘└───
581 end
st ──┘
582
583 /-- A variation around the emetric characterization of Cauchy sequences -/
584 theorem cauchy_seq_iff' [inhabited β] [semilattice_sup β] {u : β → α} :
id └───────┘ ┴ └─────────────┘ ┴ ┴ ┴
src └───────┘ └─────────────┘
typ └───────┘ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘
585 cauchy_seq u ↔ ∀ε>(0 : ennreal), ∃N, ∀n≥N, edist (u n) (u N) < ε :=
id └────────┘ ┴ ┴ ┴ └─────┘ ┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ └─────┘ ┴ ┴ └───┘ ┴
typ └────────┘ ┴ ┴ ┴ └─────┘ ┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └─────┘
586 begin
st └─────
587 rw cauchy_seq_iff,
id └────────────┘
src └─┘└────────────┘
typ └─┘└────────────┘
doc └─┘└────────────┘
txt └─┘
par └─┘
pid ┴
st ──────────────────┘└─
588 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
589 { intros H ε εpos,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ───┘└─────────────┘└─
590 rcases H ε εpos with ⟨N, hN⟩,
id ┴ ┴ └──┘
src └─────┘ ┴ ┴ └───────────┘
typ └─────┘┴┴┴┴└──┘└───────────┘
doc └─────┘ ┴ ┴ └───────────┘
txt └─────┘ ┴ ┴ └───────────┘
par └─────┘ ┴ ┴ └───────────┘
pid ┴ ┴ ┴ └───────────┘
st ───────────────────────────────┘└─
591 exact ⟨N, λn hn, hN _ _ (le_refl N) hn⟩ },
id └┘ └─────┘ ┴
src └────┘ └┘ └────┘ └───┘ └─────┘┴ └┘ └┘
typ └────┘ └┘ └────┘└┘└───┘ └─────┘┴┴└┘ └┘
doc └────┘ └┘ └────┘ └───┘ ┴ └┘ └┘
txt └────┘ └┘ └────┘ └───┘ ┴ └┘ └┘
par └────┘ └┘ └────┘ └───┘ ┴ └┘ └┘
pid ┴ └┘ └────┘ └───┘ ┴ └┘ ┴┴
st ───────────────────────────────────────────┘└┘└
592 { intros H ε εpos,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ──────────────────┘└─
593 rcases H (ε/2) (ennreal.half_pos εpos) with ⟨N, hN⟩,
id ┴ ┴┴ └──────────────┘ └──┘
src └─────┘ ┴ ┴└─┘ └──────────────┘┴ └────────────┘
typ └─────┘┴┴ ┴┴└─┘ └──────────────┘┴└──┘└────────────┘
doc └─────┘ ┴ └─┘ ┴ └────────────┘
txt └─────┘ ┴ └─┘ ┴ └────────────┘
par └─────┘ ┴ └─┘ ┴ └────────────┘
pid ┴ ┴ └─┘ ┴ └────────────┘
st ──────────────────────────────────────────────────────┘└─
594 exact ⟨N, λ m n hm hn, calc
src └────┘ └┘ └──────────┘ └
typ └────┘ └┘ └──────────┘ └
doc └────┘ └┘ └──────────┘ └
txt └────┘ └┘ └──────────┘ └
par └────┘ └┘ └──────────┘ └
pid ┴ └┘ └──────────┘ └
st ────────────────────────────────
595 edist (u n) (u m) ≤ edist (u n) (u N) + edist (u m) (u N) : edist_triangle_right _ _ _
id └───┘ ┴ ┴ └──────────────────┘
src ──────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴└───┘┴ ┴ └┘ ┴ └──┘└──────────────────┘└──────
typ ──────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴└───┘┴ ┴ └┘ ┴┴┴└──┘└──────────────────┘└──────
doc ──────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └──────
txt ──────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └──────
par ──────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └──────
pid ──────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └──────
st ──────────────────────────────────────────────────────────────────────────────────────────────
596 ... < ε/2 + ε/2 : ennreal.add_lt_add (hN _ hn) (hN _ hm)
id ┴ └────────────────┘ └┘
src ───────────────────────┘ ┴ └┘┴┴ └──┘└────────────────┘┴ └─┘ └┘ └─┘ └─
typ ───────────────────────┘ ┴ └┘┴┴ └──┘└────────────────┘┴ └─┘ └┘ └┘└─┘ └─
doc ───────────────────────┘ ┴ └┘ ┴ └──┘ ┴ └─┘ └┘ └─┘ └─
txt ───────────────────────┘ ┴ └┘ ┴ └──┘ ┴ └─┘ └┘ └─┘ └─
par ───────────────────────┘ ┴ └┘ ┴ └──┘ ┴ └─┘ └┘ └─┘ └─
pid ───────────────────────┘ ┴ └┘ ┴ └──┘ ┴ └─┘ └┘ └─┘ └─
st ─────────────────────────────────────────────────────────────────────────────
597 ... = ε : ennreal.add_halves _⟩ }
id ┴ └────────────────┘
src ───────────────────────┘ ┴ └─┘└────────────────┘└──┘
typ ───────────────────────┘ ┴┴└─┘└────────────────┘└──┘
doc ───────────────────────┘ ┴ └─┘ └──┘
txt ───────────────────────┘ ┴ └─┘ └──┘
par ───────────────────────┘ ┴ └─┘ └──┘
pid ───────────────────────┘ ┴ └─┘ └─┘┴
st ───────────────────────────────────────────────────┘└─
598 end
st ──┘
599
600 /-- A variation of the emetric characterization of Cauchy sequences that deals with
601 `nnreal` upper bounds. -/
602 theorem cauchy_seq_iff_nnreal [inhabited β] [semilattice_sup β] {u : β → α} :
id └───────┘ ┴ └─────────────┘ ┴ ┴ ┴
src └───────┘ └─────────────┘
typ └───────┘ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘
603 cauchy_seq u ↔ ∀ ε : nnreal, 0 < ε → ∃ N, ∀ n, N ≤ n → edist (u N) (u n) < ε :=
id └────────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ └────┘ ┴ ┴ ┴ ┴ └───┘ ┴
typ └────────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────┘
604 begin
st └─────
605 refine cauchy_seq_iff'.trans
id └───────────────────┘
src └─────┘└───────────────────┘└
typ └─────┘└───────────────────┘└
doc └─────┘└───────────────────┘└
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ───────────────────────────────
606 ⟨λ H ε εpos, (H ε (ennreal.coe_pos.2 εpos)).imp $
id └─────────────┘
src ───┘ └─────────┘ ┴ ┴ └─────────────┘└─┘ └─────┘ └
typ ───┘ └─────────┘ ┴ ┴ └─────────────┘└─┘ └─────┘ └
doc ───┘ └─────────┘ ┴ ┴ └─┘ └─────┘ └
txt ───┘ └─────────┘ ┴ ┴ └─┘ └─────┘ └
par ───┘ └─────────┘ ┴ ┴ └─┘ └─────┘ └
pid ───┘ └─────────┘ ┴ ┴ └─┘ └─────┘ └
st ──────────────────────────────────────────────────────
607 λ N hN n hn, edist_comm (u n) (u N) ▸ hN n hn,
id └────────┘ ┴ ┴
src ─────┘ └──────────┘└────────┘┴ ┴ └┘ ┴ └┘┴┴ ┴ ┴ └─
typ ─────┘ └──────────┘└────────┘┴ ┴ └┘ ┴┴ └┘┴┴ ┴ ┴ └─
doc ─────┘ └──────────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └─
txt ─────┘ └──────────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └─
par ─────┘ └──────────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └─
pid ─────┘ └──────────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └─
st ─────────────────────────────────────────────────────
608 λ H ε εpos, _⟩,
src ─────┘ └───────────┘
typ ─────┘ └───────────┘
doc ─────┘ └───────────┘
txt ─────┘ └───────────┘
par ─────┘ └───────────┘
pid ─────┘ └───────────┘
st ───────────────────┘└─
609 specialize H ((min 1 ε).to_nnreal)
id ┴ └─┘ ┴
src └─────────┘ ┴ └─┘└─┘ └────────────
typ └─────────┘┴┴ └─┘└─┘┴└────────────
doc └─────────┘ ┴ └─┘ └────────────
txt └─────────┘ ┴ └─┘ └────────────
par └─────────┘ ┴ └─┘ └────────────
pid ┴ ┴ └─┘ └────────────
st ─────────────────────────────────────
610 (ennreal.to_nnreal_pos_iff.2 ⟨lt_min ennreal.zero_lt_one εpos,
id └───────────────────────┘ └────┘ └─────────────────┘ └──┘
src ───┘ └───────────────────────┘└─┘ └────┘┴└─────────────────┘┴ └─
typ ───┘ └───────────────────────┘└─┘ └────┘┴└─────────────────┘┴└──┘└─
doc ───┘ └─┘ ┴ ┴ └─
txt ───┘ └─┘ ┴ ┴ └─
par ───┘ └─┘ ┴ ┴ └─
pid ───┘ └─┘ ┴ ┴ └─
st ───────────────────────────────────────────────────────────────────
611 ennreal.lt_top_iff_ne_top.1 $ min_lt_iff.2 $ or.inl ennreal.coe_lt_top⟩),
id └───────────────────────┘ └────────┘ └────┘ └────────────────┘
src ─────┘└───────────────────────┘└─┘ ┴└────────┘└─┘ ┴└────┘┴└────────────────┘└┘
typ ─────┘└───────────────────────┘└─┘ ┴└────────┘└─┘ ┴└────┘┴└────────────────┘└┘
doc ─────┘ └─┘ ┴ └─┘ ┴ ┴ └┘
txt ─────┘ └─┘ ┴ └─┘ ┴ ┴ └┘
par ─────┘ └─┘ ┴ └─┘ ┴ ┴ └┘
pid ─────┘ └─┘ ┴ └─┘ ┴ ┴ └┘
st ─────────────────────────────────────────────────────────────────────────────┘└─
612 refine H.imp (λ N hN n hn, edist_comm (u N) (u n) ▸ lt_of_lt_of_le (hN n hn) _),
id └───┘ └────────┘ ┴ └────────────┘
src └─────┘└───┘┴ └──────────┘└────────┘┴ ┴ └┘ ┴ └┘ ┴└────────────┘┴ ┴ ┴ └──┘
typ └─────┘└───┘┴ └──────────┘└────────┘┴ ┴ └┘ ┴┴ └┘ ┴└────────────┘┴ ┴ ┴ └──┘
doc └─────┘ ┴ └──────────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └──┘
txt └─────┘ ┴ └──────────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └──┘
par └─────┘ ┴ └──────────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └──┘
pid ┴ ┴ └──────────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └──┘
st ────────────────────────────────────────────────────────────────────────────────┘└─
613 refine ennreal.coe_le_iff.2 _,
id └────────────────┘
src └─────┘└────────────────┘└──┘
typ └─────┘└────────────────┘└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ──────────────────────────────┘└─
614 rintros ε rfl,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └────┘
st ──────────────┘└─
615 rw [← ennreal.coe_one, ← ennreal.coe_min, ennreal.to_nnreal_coe],
id └─────────────┘ └─────────────┘ └───────────────────┘
src └────┘└─────────────┘└──┘└─────────────┘└┘└───────────────────┘┴
typ └────┘└─────────────┘└──┘└─────────────┘└┘└───────────────────┘┴
doc └────┘ └──┘ └┘ ┴
txt └────┘ └──┘ └┘ ┴
par └────┘ └──┘ └┘ ┴
pid └──┘ └──┘ └┘ ┴
st ──────────────────────┘└─────────────────┘└─────────────────────┘└──
616 apply min_le_right
id └──────────┘
src └────┘└──────────┘┴
typ └────┘└──────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────┘
617 end
st └─┘
618
619 theorem totally_bounded_iff {s : set α} :
id └─┘ ┴
src └─┘
typ └─┘ ┴
620 totally_bounded s ↔ ∀ ε > 0, ∃t : set α, finite t ∧ s ⊆ ⋃y∈t, ball y ε :=
id └─────────────┘ ┴ ┴ ┴ ┴ └─┘ ┴┴ └────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴
src └─────────────┘ ┴ ┴ └─┘ ┴ └────┘ ┴ ┴ ┴ ┴ └──┘
typ └─────────────┘ ┴ ┴ ┴ ┴ └─┘ ┴┴ └────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴
doc └─────────────┘ └────┘ ┴ ┴ └──┘
621 ⟨λ H ε ε0, H _ (edist_mem_uniformity ε0),
id ┴ ┴ └┘ ┴ └──────────────────┘ └┘
src └──────────────────┘
typ ┴ ┴ └┘ ┴ └──────────────────┘ └┘
doc └──────────────────┘
622 λ H r ru, let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru,
id ┴ ┴ └┘ └─┘ ┴ └┘ └┘ └──────────────────┘┴ └┘
src └──────────────────┘┴
typ ┴ ┴ └┘ └─┘ ┴ └┘ └┘ └──────────────────┘┴ └┘
doc └──────────────────┘
623 ⟨t, ft, h⟩ := H ε ε0 in
id ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴
624 ⟨t, ft, subset.trans h $ Union_subset_Union $ λ y, Union_subset_Union $ λ yt z, hε⟩⟩
id └──────────┘ └────────────────┘ ┴ └────────────────┘ └┘ ┴
src └──────────┘ └────────────────┘ └────────────────┘
typ └──────────┘ └────────────────┘ ┴ └────────────────┘ └┘ ┴
625
626 theorem totally_bounded_iff' {s : set α} :
id └─┘ ┴
src └─┘
typ └─┘ ┴
627 totally_bounded s ↔ ∀ ε > 0, ∃t⊆s, finite t ∧ s ⊆ ⋃y∈t, ball y ε :=
id └─────────────┘ ┴ ┴ ┴ ┴┴ ┴┴ └────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴
src └─────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └──┘
typ └─────────────┘ ┴ ┴ ┴ ┴┴ ┴┴ └────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴
doc └─────────────┘ └────┘ ┴ ┴ └──┘
628 ⟨λ H ε ε0, (totally_bounded_iff_subset.1 H) _ (edist_mem_uniformity ε0),
id ┴ ┴ └┘ └────────────────────────┘┴ ┴ └──────────────────┘ └┘
src └────────────────────────┘┴ └──────────────────┘
typ ┴ ┴ └┘ └────────────────────────┘┴ ┴ └──────────────────┘ └┘
doc └──────────────────┘
629 λ H r ru, let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru,
id ┴ ┴ └┘ └─┘ ┴ └┘ └┘ └──────────────────┘┴ └┘
src └──────────────────┘┴
typ ┴ ┴ └┘ └─┘ ┴ └┘ └┘ └──────────────────┘┴ └┘
doc └──────────────────┘
630 ⟨t, _, ft, h⟩ := H ε ε0 in
id ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴
631 ⟨t, ft, subset.trans h $ Union_subset_Union $ λ y, Union_subset_Union $ λ yt z, hε⟩⟩
id └──────────┘ └────────────────┘ ┴ └────────────────┘ └┘ ┴
src └──────────┘ └────────────────┘ └────────────────┘
typ └──────────┘ └────────────────┘ ┴ └────────────────┘ └┘ ┴
632
633 section compact
634
635 /-- A compact set in an emetric space is separable, i.e., it is the closure of a countable set -/
636 lemma countable_closure_of_compact {α : Type u} [emetric_space α] {s : set α} (hs : compact s) :
id └───────────┘ ┴ └─┘ ┴ └─────┘ ┴
src └───────────┘ └─┘ └─────┘
typ └───────────┘ ┴ └─┘ ┴ └─────┘ ┴
doc └───────────┘ └─────┘
637 ∃ t ⊆ s, (countable t ∧ s = closure t) :=
id ┴ ┴ ┴┴ └───────┘ ┴ ┴ ┴ ┴ └─────┘ ┴
src ┴ ┴ └───────┘ ┴ ┴ └─────┘
typ ┴ ┴ ┴┴ └───────┘ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └───────┘ └─────┘
638 begin
st └─────
639 have A : ∀ (e:ennreal), e > 0 → ∃ t ⊆ s, (finite t ∧ s ⊆ (⋃x∈t, ball x e)) :=
id └─────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └──┘
src └───────┘ └──┘└─────┘┴ ┴ ┴┴└─┘ ┴┴└───┘ ┴┴ └────┘┴ ┴ ┴ ┴ ┴ ┴└┘ ┴┴└──┘┴ ┴ └─────
typ └───────┘ └──┘└─────┘┴ ┴ ┴┴└─┘ ┴┴└───┘ ┴┴ └────┘┴ ┴ ┴┴┴ ┴ ┴└┘ ┴┴└──┘┴ ┴ └─────
doc └───────┘ └──┘└─────┘┴ ┴ ┴ └─┘ ┴ └───┘ ┴ └────┘┴ ┴ ┴ ┴ ┴ ┴└┘ ┴┴└──┘┴ ┴ └─────
txt └───────┘ └──┘ ┴ ┴ ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─────
par └───────┘ └──┘ ┴ ┴ ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─────
pid └────┘└─┘ └──┘ ┴ ┴ ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘└───
st ────────────────────────────────────────────────────────────────────────────────
640 totally_bounded_iff'.1 (compact_iff_totally_bounded_complete.1 hs).1,
id └──────────────────┘ └──────────────────────────────────┘ └┘
src ───┘└──────────────────┘└─┘ └──────────────────────────────────┘└─┘ └─┘
typ ───┘└──────────────────┘└─┘ └──────────────────────────────────┘└─┘└┘└─┘
doc ───┘ └─┘ └─┘ └─┘
txt ───┘ └─┘ └─┘ └─┘
par ───┘ └─┘ └─┘ └─┘
pid ───┘ └─┘ └─┘ ┴└┘
st ───────────────────────────────────────────────────────────────────────┘└─
641 -- assume e, finite_cover_balls_of_compact hs,
st ──────────────────────────────────────────────────
642 have B : ∀ (e:ennreal), ∃ t ⊆ s, finite t ∧ (e > 0 → s ⊆ (⋃x∈t, ball x e)),
id └─────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └──┘
src └───────┘ └──┘└─────┘┴ ┴┴└───┘ ┴┴└────┘┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴└┘ ┴┴└──┘┴ ┴ └┘
typ └───────┘ └──┘└─────┘┴ ┴┴└───┘ ┴┴└────┘┴ ┴ ┴ ┴┴└─┘ ┴┴┴ ┴ ┴└┘ ┴┴└──┘┴ ┴ └┘
doc └───────┘ └──┘└─────┘┴ ┴ └───┘ ┴└────┘┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴└┘ ┴┴└──┘┴ ┴ └┘
txt └───────┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
par └───────┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
pid └────┘└─┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────┘└─
643 { intro e,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ───┘└─────┘└─
644 cases le_or_gt e 0 with h,
id └──────┘ ┴
src └────┘└──────┘┴ └───────┘
typ └────┘└──────┘┴┴└───────┘
doc └────┘ ┴ └───────┘
txt └────┘ ┴ └───────┘
par └────┘ ┴ └───────┘
pid ┴ ┴ ┴└──────┘
st ────────────────────────────┘└─
645 { exact ⟨∅, by finish⟩ },
id ┴
src └────┘ ┴└┘ ┴└────┘└┘
typ └────┘ ┴└┘ ┴└────┘└┘
doc └────┘ └┘ ┴└────┘└┘
txt └────┘ └┘ ┴└────┘└┘
par └────┘ └┘ ┴└────┘└┘
pid ┴ └┘ └──────┘┴
st ─────┘└──────────┘└─────┘└┘└┘└
646 { rcases A e h with ⟨s, ⟨finite_s, closure_s⟩⟩, existsi s, finish }},
id ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ └──────────────────────────────┘ └──────┘ └─────┘
typ └─────┘┴┴┴┴┴└──────────────────────────────┘ └──────┘┴ └─────┘
doc └─────┘ ┴ ┴ └──────────────────────────────┘ └──────┘ └─────┘
txt └─────┘ ┴ ┴ └──────────────────────────────┘ └──────┘ └─────┘
par └─────┘ ┴ ┴ └──────────────────────────────┘ └──────┘ └─────┘
pid ┴ ┴ ┴ └──────────────────────────────┘ ┴ ┴
st ─────────────────────────────────────────────────┘└─────────┘└───────┘└─┘└
647 /-The desired countable set is obtained by taking for each `n` the centers of a finite cover
st ───────────────────────────────────────────────────────────────────────────────────────────────
648 by balls of radius `1/n`, and then the union over `n`. -/
st ────────────────────────────────────────────────────────────
649 choose T T_in_s finite_T using B,
id ┴
src └─────────────────────────────┘
typ └─────────────────────────────┘┴
doc └─────────────────────────────┘
txt └─────────────────────────────┘
par └─────────────────────────────┘
pid └┘└──────────────┘└─────┘
st ─────────────────────────────────┘└─
650 let t := ⋃n:ℕ, T n⁻¹,
id ┴ ┴ ┴ └┘
src └───────┘┴└┘ ┴┴ ┴ └┘
typ └───────┘┴└┘ ┴┴┴┴ └┘
doc └───────┘┴└┘ ┴┴ ┴
txt └───────┘ └┘ ┴ ┴
par └───────┘ └┘ ┴ ┴
pid └───┘┴└─┘ └┘ ┴ ┴
st ─────────────────────┘└─
651 have T₁ : t ⊆ s := begin apply Union_subset, assume n, apply T_in_s end,
id ┴ ┴ └──────────┘
src └────────┘ ┴ ┴ └──┘ ┴└────┘└──────────┘└┘└──────┘└┘└────┘ ┴└─┘
typ └────────┘┴┴ ┴┴└──┘ ┴└────┘└──────────┘└┘└──────┘└┘└────┘ ┴└─┘
doc └────────┘ ┴ ┴ └──┘ ┴└────┘ └┘└──────┘└┘└────┘ ┴└─┘
txt └────────┘ ┴ ┴ └──┘ ┴└────┘ └┘└──────┘└┘└────┘ ┴└─┘
par └────────┘ ┴ ┴ └──┘ ┴└────┘ └┘└──────┘└┘└────┘ ┴└─┘
pid └─────┘└─┘ ┴ ┴ └──┘ └─────┘ └────────────────┘ └──┘
st ────────────────────┘└──────────────────────┘└────────┘└─────────────┘└─┘└─
652 have T₂ : countable t := by finish [countable_Union, countable_finite],
id └───────┘ ┴ └─────────────┘ └──────────────┘
src └────────┘└───────┘┴ └──┘ ┴└──────┘└─────────────┘└┘└──────────────┘┴
typ └────────┘└───────┘┴┴└──┘ ┴└──────┘└─────────────┘└┘└──────────────┘┴
doc └────────┘└───────┘┴ └──┘ ┴└──────┘ └┘ ┴
txt └────────┘ ┴ └──┘ ┴└──────┘ └┘ ┴
par └────────┘ ┴ └──┘ ┴└──────┘ └┘ ┴
pid └─────┘└─┘ ┴ └──┘ └───────┘ └┘ ┴
st ────────────────────────────┘└─────────────────────────────────────────┘└─
653 have T₃ : s ⊆ closure t,
id ┴ └─────┘ ┴
src └────────┘ ┴ ┴└─────┘┴
typ └────────┘┴┴ ┴└─────┘┴┴
doc └────────┘ ┴ ┴└─────┘┴
txt └────────┘ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴
pid └─────┘└─┘ ┴ ┴ ┴
st ────────────────────────┘└─
654 { intros x x_in_s,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ───┘└─────────────┘└─
655 apply mem_closure_iff'.2,
id └──────────────┘
src └────┘└──────────────┘└┘
typ └────┘└──────────────┘└┘
doc └────┘└──────────────┘└┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ───────────────────────────┘└─
656 intros ε εpos,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ────────────────┘└─
657 rcases ennreal.exists_inv_nat_lt (bot_lt_iff_ne_bot.1 εpos) with ⟨n, hn⟩,
id └───────────────────────┘ └───────────────┘ └──┘
src └─────┘└───────────────────────┘┴ └───────────────┘└─┘ └────────────┘
typ └─────┘└───────────────────────┘┴ └───────────────┘└─┘└──┘└────────────┘
doc └─────┘ ┴ └─┘ └────────────┘
txt └─────┘ ┴ └─┘ └────────────┘
par └─────┘ ┴ └─┘ └────────────┘
pid ┴ ┴ └─┘ └────────────┘
st ───────────────────────────────────────────────────────────────────────────┘└─
658 have inv_n_pos : (0 : ennreal) < (n : ℕ)⁻¹ := by simp [ennreal.bot_lt_iff_ne_bot],
id └─────┘ ┴ └┘ └───────────────────────┘
src └───────────────┘ └──┘└─────┘└┘┴┴ └─┘ ┴ └──┘ ┴└────┘└───────────────────────┘┴
typ └───────────────┘ └──┘└─────┘└┘┴┴└┘└─┘ ┴ └──┘ ┴└────┘└───────────────────────┘┴
doc └───────────────┘ └──┘└─────┘└┘ ┴ └─┘ ┴ └──┘ ┴└────┘ ┴
txt └───────────────┘ └──┘ └┘ ┴ └─┘ ┴ └──┘ ┴└────┘ ┴
par └───────────────┘ └──┘ └┘ ┴ └─┘ ┴ └──┘ ┴└────┘ ┴
pid └────────────┘└─┘ └──┘ └┘ ┴ └─┘ ┴ └──┘ └─────┘ ┴
st ───────────────────────────────────────────────────┘└───────────────────────────────┘└─
659 have C : x ∈ (⋃y∈ T (n : ℕ)⁻¹, ball y (n : ℕ)⁻¹) :=
id ┴ ┴ ┴ ┴ └──┘ ┴
src └───────┘ ┴ ┴ ┴└─┘ ┴ └─┘ ┴ ┴┴└──┘┴ ┴ └─┘ ┴ └────
typ └───────┘┴┴ ┴ ┴└─┘┴┴ └─┘ ┴ ┴┴└──┘┴ ┴ ┴└─┘ ┴ └────
doc └───────┘ ┴ ┴ ┴└─┘ ┴ └─┘ ┴ ┴┴└──┘┴ ┴ └─┘ ┴ └────
txt └───────┘ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
par └───────┘ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
pid └────┘└─┘ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴└───
st ────────────────────────────────────────────────────────
660 mem_of_mem_of_subset x_in_s ((finite_T (n : ℕ)⁻¹).2 inv_n_pos),
id └──────────────────┘ └────┘ └──────┘ ┴ └───────┘
src ─────┘└──────────────────┘┴ ┴ ┴ └─┘ ┴ └──┘ ┴
typ ─────┘└──────────────────┘┴└────┘┴ └──────┘┴ ┴└─┘ ┴ └──┘└───────┘┴
doc ─────┘ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴
txt ─────┘ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴
par ─────┘ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴
pid ─────┘ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴
st ───────────────────────────────────────────────────────────────────┘└─
661 rcases mem_Union.1 C with ⟨y, _, ⟨y_in_T, rfl⟩, Dxy⟩,
id └───────┘ ┴
src └─────┘└───────┘└─┘ └──────────────────────────────┘
typ └─────┘└───────┘└─┘┴└──────────────────────────────┘
doc └─────┘ └─┘ └──────────────────────────────┘
txt └─────┘ └─┘ └──────────────────────────────┘
par └─────┘ └─┘ └──────────────────────────────┘
pid ┴ └─┘ └──────────────────────────────┘
st ───────────────────────────────────────────────────────┘└─
662 simp at Dxy, -- Dxy : edist x y < 1 / ↑n
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid ┴└────┘
st ──────────────┘└──────────────────────────────
663 have : y ∈ t := mem_of_mem_of_subset y_in_T (by apply subset_Union (λ (n:ℕ), T (n : ℕ)⁻¹)),
id ┴ ┴ └──────────────────┘ └────┘ └──────────┘ ┴
src └─────┘ ┴ ┴ └──┘└──────────────────┘┴ ┴ ┴└────┘└──────────┘┴ └──┘ └─┘ ┴ └─┘ ┴ ┴┴
typ └─────┘┴┴ ┴┴└──┘└──────────────────┘┴└────┘┴ ┴└────┘└──────────┘┴ └──┘ └─┘┴┴ └─┘ ┴ ┴┴
doc └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴└────┘ ┴ └──┘ └─┘ ┴ └─┘ ┴ ┴┴
txt └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴└────┘ ┴ └──┘ └─┘ ┴ └─┘ ┴ ┴┴
par └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴└────┘ ┴ └──┘ └─┘ ┴ └─┘ ┴ ┴┴
pid └───┘└┘ ┴ ┴ └──┘ ┴ ┴ └─────┘ ┴ └──┘ └─┘ ┴ └─┘ ┴ └┘
st ──────────────────────────────────────────────────┘└────────────────────────────────────────┘┴└─
664 have : edist x y < ε := lt_trans Dxy hn,
id └───┘ ┴ ┴ ┴ └──────┘ └─┘ └┘
src └─────┘└───┘┴ ┴ ┴ ┴ └──┘└──────┘┴ ┴
typ └─────┘└───┘┴┴┴┴┴ ┴┴└──┘└──────┘┴└─┘┴└┘
doc └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
st ──────────────────────────────────────────┘└─
665 exact ⟨y, ‹y ∈ t›, ‹edist x y < ε›⟩ },
id ┴ ┴┴ └───┘ ┴ ┴ ┴
src └────┘ └┘┴ ┴ ┴ ┴└┘ └───┘┴ ┴ ┴ ┴ └┘
typ └────┘ └┘┴ ┴ ┴┴┴└┘ └───┘┴┴┴┴┴ ┴┴ └┘
doc └────┘ └┘┴ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ └┘
txt └────┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
par └────┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
pid ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴
st ───────────────────────────────────────┘└┘└
666 have T₄ : closure t ⊆ s := calc
id └─────┘ ┴ ┴
src └────────┘└─────┘┴ ┴ ┴ └──┘ └
typ └────────┘└─────┘┴┴┴ ┴┴└──┘ └
doc └────────┘└─────┘┴ ┴ ┴ └──┘ └
txt └────────┘ ┴ ┴ ┴ └──┘ └
par └────────┘ ┴ ┴ ┴ └──┘ └
pid └─────┘└─┘ ┴ ┴ ┴ └──┘ └
st ──────────────────────────────────
667 closure t ⊆ closure s : closure_mono T₁
id ┴ └─────┘ └──────────┘ └┘
src ───┘ ┴ ┴ ┴└─────┘┴ └─┘└──────────┘┴ └
typ ───┘ ┴┴┴ ┴└─────┘┴ └─┘└──────────┘┴└┘└
doc ───┘ ┴ ┴ ┴└─────┘┴ └─┘ ┴ └
txt ───┘ ┴ ┴ ┴ ┴ └─┘ ┴ └
par ───┘ ┴ ┴ ┴ ┴ └─┘ ┴ └
pid ───┘ ┴ ┴ ┴ ┴ └─┘ ┴ └
st ────────────────────────────────────────────
668 ... = s : closure_eq_of_is_closed (closed_of_compact _ hs),
id ┴ └─────────────────────┘ └───────────────┘ └┘
src ───────┘ ┴ └─┘└─────────────────────┘┴ └───────────────┘└─┘ ┴
typ ───────┘ ┴┴└─┘└─────────────────────┘┴ └───────────────┘└─┘└┘┴
doc ───────┘ ┴ └─┘ ┴ └─┘ ┴
txt ───────┘ ┴ └─┘ ┴ └─┘ ┴
par ───────┘ ┴ └─┘ ┴ └─┘ ┴
pid ───────┘ ┴ └─┘ ┴ └─┘ ┴
st ─────────────────────────────────────────────────────────────┘└─
669 exact ⟨t, ⟨T₁, T₂, subset.antisymm T₃ T₄⟩⟩
id ┴ └┘ └┘ └─────────────┘ └┘ └┘
src └────┘ └┘ └┘ └┘└─────────────┘┴ ┴ └─┘
typ └────┘ ┴└┘ └┘└┘└┘└┘└─────────────┘┴└┘┴└┘└─┘
doc └────┘ └┘ └┘ └┘ ┴ ┴ └─┘
txt └────┘ └┘ └┘ └┘ ┴ ┴ └─┘
par └────┘ └┘ └┘ └┘ ┴ ┴ └─┘
pid ┴ └┘ └┘ └┘ ┴ ┴ └┘┴
st ────────────────────────────────────────────┘
670 end
st └─┘
671
672 end compact
673
674 section first_countable
675
676 @[priority 100] -- see Note [lower instance priority]
677 instance (α : Type u) [emetric_space α] :
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
doc └───────────┘
678 topological_space.first_countable_topology α :=
id └────────────────────────────────────────┘ ┴
src └────────────────────────────────────────┘
typ └────────────────────────────────────────┘ ┴
doc └────────────────────────────────────────┘
679 uniform_space.first_countable_topology uniformity_has_countable_basis
id └────────────────────────────────────┘ └────────────────────────────┘
src └────────────────────────────────────┘ └────────────────────────────┘
typ └────────────────────────────────────┘ └────────────────────────────┘
680
681 end first_countable
682
683 section second_countable
684 open topological_space
685
686 /-- A separable emetric space is second countable: one obtains a countable basis by taking
687 the balls centered at points in a dense subset, and with rational radii. We do not register
688 this as an instance, as there is already an instance going in the other direction
689 from second countable spaces to separable spaces, and we want to avoid loops. -/
690 lemma second_countable_of_separable (α : Type u) [emetric_space α] [separable_space α] :
id └───────────┘ ┴ └─────────────┘ ┴
src └───────────┘ └─────────────┘
typ └───────────┘ ┴ └─────────────┘ ┴
doc └───────────┘ └─────────────┘
691 second_countable_topology α :=
id └───────────────────────┘ ┴
src └───────────────────────┘
typ └───────────────────────┘ ┴
doc └───────────────────────┘
692 let ⟨S, ⟨S_countable, S_dense⟩⟩ := separable_space.exists_countable_closure_eq_univ α in
id └─┘ ┴ └──────────────────────────────────────────────┘ ┴
src └──────────────────────────────────────────────┘
typ └─┘ ┴ └──────────────────────────────────────────────┘ ┴
693 ⟨⟨⋃x ∈ S, ⋃ (n : nat), {ball x (n⁻¹)},
id ┴┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└┘
src ┴ ┴ ┴ └─┘ ┴ ┴└──┘ └┘
typ ┴┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└┘
doc ┴ ┴ ┴ ┴ └──┘
694 ⟨show countable ⋃x ∈ S, ⋃ (n : nat), {ball x (n⁻¹)},
id └───────┘ ┴┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└┘
src └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴└──┘ └┘
typ └───────┘ ┴┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└┘
doc └───────┘ ┴ ┴ ┴ ┴ └──┘
695 { apply countable_bUnion S_countable,
id └──────────────┘ └─────────┘
src └────┘└──────────────┘┴
typ └────┘└──────────────┘┴└─────────┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st └──────────────────────────────────┘└─
696 intros a aS,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
697 apply countable_Union,
id └─────────────┘
src └────┘└─────────────┘
typ └────┘└─────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────┘└─
698 simp },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────┘└┘
699 show uniform_space.to_topological_space α = generate_from (⋃x ∈ S, ⋃ (n : nat), {ball x (n⁻¹)}),
id └────────────────────────────────┘ ┴ ┴ └───────────┘ ┴┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└┘
src └────────────────────────────────┘ ┴ └───────────┘ ┴ ┴ ┴ └─┘ ┴ ┴└──┘ └┘
typ └────────────────────────────────┘ ┴ ┴ └───────────┘ ┴┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└┘
doc └───────────┘ ┴ ┴ ┴ ┴ └──┘
700 { have A : ∀ (u : set α), (u ∈ ⋃x ∈ S, ⋃ (n : nat), ({ball x ((n : ennreal)⁻¹)} : set (set α))) → is_open u,
id └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─────┘ └┘ └─┘ ┴ └─────┘
src └───────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴┴└────┘└─┘┴┴┴ ┴└───┘ ┴ └─┘└─────┘┴└┘└───┘ ┴ └─┘┴ └──┘ ┴└─────┘┴
typ └───────┘ └────┘└─┘┴ ┴ ┴ ┴┴┴ └──┘┴ ┴┴└────┘└─┘┴┴┴ ┴└───┘ ┴ └─┘└─────┘┴└┘└───┘ ┴ └─┘┴┴└──┘ ┴└─────┘┴
doc └───────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴┴└────┘ ┴┴┴ └───┘ ┴ └─┘└─────┘┴ └───┘ ┴ ┴ └──┘ ┴└─────┘┴
txt └───────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └────┘ ┴ ┴ └───┘ ┴ └─┘ ┴ └───┘ ┴ ┴ └──┘ ┴ ┴
par └───────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └────┘ ┴ ┴ └───┘ ┴ └─┘ ┴ └───┘ ┴ ┴ └──┘ ┴ ┴
pid └────┘└─┘ └────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └────┘ ┴ ┴ └───┘ ┴ └─┘ ┴ └───┘ ┴ ┴ └──┘ ┴ ┴
st └─────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
701 { simp only [and_imp, exists_prop, set.mem_Union, set.mem_singleton_iff, exists_imp_distrib],
id └─────┘ └─────────┘ └───────────┘ └───────────────────┘ └────────────────┘
src └─────────┘└─────┘└┘└─────────┘└┘└───────────┘└┘└───────────────────┘└┘└────────────────┘┴
typ └─────────┘└─────┘└┘└─────────┘└┘└───────────┘└┘└───────────────────┘└┘└────────────────┘┴
doc └─────────┘ └┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴
st ───┘└────────────────────────────────────────────────────────────────────────────────────────┘└─
702 intros u x hx i u_ball,
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid └──────────────┘
st ─────────────────────────┘└─
703 rw [u_ball],
id └────┘
src └──┘ ┴
typ └──┘└────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ─────────────┘└──
704 exact is_open_ball },
id └──────────┘
src └────┘└──────────┘┴
typ └────┘└──────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────┘└┘└
705 have B : is_topological_basis (⋃x ∈ S, ⋃ (n : nat), ({ball x (n⁻¹)} : set (set α))),
id └──────────────────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └───────┘└──────────────────┘┴ └──┘ ┴┴└────┘└─┘┴┴┴ ┴└───┘ ┴ └───┘ ┴ └─┘┴ └─┘
typ └───────┘└──────────────────┘┴ └──┘┴ ┴┴└────┘└─┘┴┴┴ ┴└───┘ ┴ └───┘ ┴ └─┘┴┴└─┘
doc └───────┘└──────────────────┘┴ └──┘ ┴┴└────┘ ┴┴┴ └───┘ ┴ └───┘ ┴ ┴ └─┘
txt └───────┘ ┴ └──┘ ┴ └────┘ ┴ ┴ └───┘ ┴ └───┘ ┴ ┴ └─┘
par └───────┘ ┴ └──┘ ┴ └────┘ ┴ ┴ └───┘ ┴ └───┘ ┴ ┴ └─┘
pid └────┘└─┘ ┴ └──┘ ┴ └────┘ ┴ ┴ └───┘ ┴ └───┘ ┴ ┴ └─┘
st ────────────────────────────────────────────────────────────────────────────────────┘└─
706 { refine is_topological_basis_of_open_of_nhds A (λa u au open_u, _),
id └──────────────────────────────────┘ ┴
src └─────┘└──────────────────────────────────┘┴ ┴ └───────────────┘
typ └─────┘└──────────────────────────────────┘┴┴┴ └───────────────┘
doc └─────┘ ┴ ┴ └───────────────┘
txt └─────┘ ┴ ┴ └───────────────┘
par └─────┘ ┴ ┴ └───────────────┘
pid ┴ ┴ ┴ └───────────────┘
st ───┘└───────────────────────────────────────────────────────────────┘└─
707 rcases is_open_iff.1 open_u a au with ⟨ε, εpos, εball⟩,
id └─────────┘ └────┘ ┴ └┘
src └─────┘└─────────┘└─┘ ┴ ┴ └────────────────────┘
typ └─────┘└─────────┘└─┘└────┘┴┴┴└┘└────────────────────┘
doc └─────┘ └─┘ ┴ ┴ └────────────────────┘
txt └─────┘ └─┘ ┴ ┴ └────────────────────┘
par └─────┘ └─┘ ┴ ┴ └────────────────────┘
pid ┴ └─┘ ┴ ┴ └────────────────────┘
st ─────────────────────────────────────────────────────────┘└─
708 have : ε / 2 > 0 := ennreal.half_pos εpos,
id ┴ ┴ ┴ └──────────────┘ └──┘
src └─────┘ ┴┴└─┘┴└────┘└──────────────┘┴
typ └─────┘┴┴┴└─┘┴└────┘└──────────────┘┴└──┘
doc └─────┘ ┴ └─┘ └────┘ ┴
txt └─────┘ ┴ └─┘ └────┘ ┴
par └─────┘ ┴ └─┘ └────┘ ┴
pid └───┘└┘ ┴ └─┘ ┴└───┘ ┴
st ────────────────────────────────────────────┘└─
709 /- The ball `ball a ε` is included in `u`. We need to find one of our balls `ball x (n⁻¹)`
st ───────────────────────────────────────────────────────────────────────────────────────────────
710 containing `a` and contained in `ball a ε`. For this, we take `n` larger than `2/ε`, and
st ─────────────────────────────────────────────────────────────────────────────────────────────
711 then `x` in `S` at distance at most `n⁻¹` of `a` -/
st ────────────────────────────────────────────────────────
712 rcases ennreal.exists_inv_nat_lt (bot_lt_iff_ne_bot.1 (ennreal.half_pos εpos)) with ⟨n, εn⟩,
id └───────────────────────┘ └───────────────┘ └──────────────┘ └──┘
src └─────┘└───────────────────────┘┴ └───────────────┘└─┘ └──────────────┘┴ └─────────────┘
typ └─────┘└───────────────────────┘┴ └───────────────┘└─┘ └──────────────┘┴└──┘└─────────────┘
doc └─────┘ ┴ └─┘ ┴ └─────────────┘
txt └─────┘ ┴ └─┘ ┴ └─────────────┘
par └─────┘ ┴ └─┘ ┴ └─────────────┘
pid ┴ ┴ └─┘ ┴ └─────────────┘
st ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
713 have : (0 : ennreal) < n⁻¹ := by simp [ennreal.bot_lt_iff_ne_bot],
id └─────┘ ┴ ┴ └───────────────────────┘
src └─────┘ └──┘└─────┘└┘┴┴ └──┘ ┴└────┘└───────────────────────┘┴
typ └─────┘ └──┘└─────┘└┘┴┴┴ └──┘ ┴└────┘└───────────────────────┘┴
doc └─────┘ └──┘└─────┘└┘ ┴ └──┘ ┴└────┘ ┴
txt └─────┘ └──┘ └┘ ┴ └──┘ ┴└────┘ ┴
par └─────┘ └──┘ └┘ ┴ └──┘ ┴└────┘ ┴
pid └───┘└┘ └──┘ └┘ ┴ └──┘ └─────┘ ┴
st ───────────────────────────────────┘└───────────────────────────────┘└─
714 have : (a : α) ∈ closure (S : set α) := by rw [S_dense]; simp,
id ┴ └─────┘ ┴ └─┘ ┴ └─────┘
src └─────┘ └─┘ └┘ ┴└─────┘┴ └─┘└─┘┴ └───┘ ┴└──┘ ┴└┘└──┘
typ └─────┘ ┴└─┘ └┘ ┴└─────┘┴ ┴└─┘└─┘┴┴└───┘ ┴└──┘└─────┘┴└┘└──┘
doc └─────┘ └─┘ └┘ ┴└─────┘┴ └─┘ ┴ └───┘ ┴└──┘ ┴└┘└──┘
txt └─────┘ └─┘ └┘ ┴ ┴ └─┘ ┴ └───┘ ┴└──┘ ┴└┘└──┘
par └─────┘ └─┘ └┘ ┴ ┴ └─┘ ┴ └───┘ ┴└──┘ ┴└┘└──┘
pid └───┘└┘ └─┘ └┘ ┴ ┴ └─┘ ┴ ┴└──┘ └───┘ └─────┘
st ─────────────────────────────────────────────┘└──────────┘┴└────┘└─
715 rcases mem_closure_iff'.1 this _ ‹(0 : ennreal) < n⁻¹› with ⟨x, xS, xdist⟩,
id └──────────────┘ └──┘ ┴ └─────┘ ┴ ┴
src └─────┘└──────────────┘└─┘ └─┘┴ └──┘└─────┘└┘ └┘ ┴└──────────────────┘
typ └─────┘└──────────────┘└─┘└──┘└─┘┴ └──┘└─────┘└┘ └┘┴ ┴└──────────────────┘
doc └─────┘└──────────────┘└─┘ └─┘┴ └──┘└─────┘└┘ └┘ ┴└──────────────────┘
txt └─────┘ └─┘ └─┘ └──┘ └┘ └┘ └──────────────────┘
par └─────┘ └─┘ └─┘ └──┘ └┘ └┘ └──────────────────┘
pid ┴ └─┘ └─┘ └──┘ └┘ └┘ └──────────────────┘
st ──────────────────────────────────────────────────────────────────────────────┘└─
716 existsi ball x (↑n)⁻¹,
id └──┘ ┴ ┴┴
src └──────┘└──┘┴ ┴ ┴ ┴
typ └──────┘└──┘┴┴┴ ┴┴┴
doc └──────┘└──┘┴ ┴ ┴
txt └──────┘ ┴ ┴ ┴
par └──────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────────┘└─
717 have I : ball x (n⁻¹) ⊆ ball a ε := λy ydist, calc
id ┴ ┴ ┴ └──┘ ┴ ┴
src └───────┘ ┴ ┴ └┘┴┴└──┘┴ ┴ └──┘ └───────┘ └
typ └───────┘ ┴┴┴ ┴ └┘┴┴└──┘┴┴┴┴└──┘ └───────┘ └
doc └───────┘ ┴ ┴ └┘ ┴└──┘┴ ┴ └──┘ └───────┘ └
txt └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └───────┘ └
par └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └───────┘ └
pid └────┘└─┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └───────┘ └
st ───────────────────────────────────────────────────────
718 edist y a = edist a y : edist_comm _ _
id └───┘ ┴ └────────┘
src ─────┘ ┴ ┴ ┴ ┴└───┘┴ ┴ └─┘└────────┘└────
typ ─────┘ ┴ ┴ ┴ ┴└───┘┴┴┴ └─┘└────────┘└────
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────
st ─────────────────────────────────────────────
719 ... ≤ edist a x + edist y x : edist_triangle_right _ _ _
id ┴ └──────────────────┘
src ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└──────────────────┘└──────
typ ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴└─┘└──────────────────┘└──────
doc ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
txt ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
par ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
st ───────────────────────────────────────────────────────────────
720 ... < n⁻¹ + n⁻¹ : ennreal.add_lt_add xdist ydist
id ┴ └───┘
src ─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └
typ ─────────┘ ┴ ┴ ┴┴ └─┘ ┴└───┘┴ └
doc ─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └
txt ─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └
par ─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └
pid ─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └
st ───────────────────────────────────────────────────────
721 ... < ε/2 + ε/2 : ennreal.add_lt_add εn εn
id ┴ └────────────────┘ └┘
src ─────────┘ ┴ └┘┴┴ └──┘└────────────────┘┴ ┴ └
typ ─────────┘ ┴ └┘┴┴ └──┘└────────────────┘┴ ┴└┘└
doc ─────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
txt ─────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
par ─────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
pid ─────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
st ─────────────────────────────────────────────────
722 ... = ε : ennreal.add_halves _,
id ┴ └────────────────┘
src ─────────┘ ┴ └─┘└────────────────┘└┘
typ ─────────┘ ┴┴└─┘└────────────────┘└┘
doc ─────────┘ ┴ └─┘ └┘
txt ─────────┘ ┴ └─┘ └┘
par ─────────┘ ┴ └─┘ └┘
pid ─────────┘ ┴ └─┘ └┘
st ───────────────────────────────────┘└─
723 simp only [emetric.mem_ball, exists_prop, set.mem_Union, set.mem_singleton_iff],
id └──────────────┘ └─────────┘ └───────────┘ └───────────────────┘
src └─────────┘└──────────────┘└┘└─────────┘└┘└───────────┘└┘└───────────────────┘┴
typ └─────────┘└──────────────┘└┘└─────────┘└┘└───────────┘└┘└───────────────────┘┴
doc └─────────┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ ┴
st ──────────────────────────────────────────────────────────────────────────────────┘└─
724 exact ⟨⟨x, ⟨xS, ⟨n, rfl⟩⟩⟩, ⟨by simpa, subset.trans I εball⟩⟩ },
id ┴ └┘ ┴ └─┘ └──────────┘ ┴ └───┘
src └────┘ └┘ └┘ └┘└─┘└───┘ ┴└───┘└┘└──────────┘┴ ┴ └─┘
typ └────┘ ┴└┘ └┘└┘ ┴└┘└─┘└───┘ ┴└───┘└┘└──────────┘┴┴┴└───┘└─┘
doc └────┘ └┘ └┘ └┘ └───┘ ┴└───┘└┘ ┴ ┴ └─┘
txt └────┘ └┘ └┘ └┘ └───┘ ┴└───┘└┘ ┴ ┴ └─┘
par └────┘ └┘ └┘ └┘ └───┘ ┴└───┘└┘ ┴ ┴ └─┘
pid ┴ └┘ └┘ └┘ └───┘ └──────┘ ┴ ┴ └┘┴
st ──────────────────────────────────┘└────┘└───────────────────────┘└┘└
725 exact B.2.2 }⟩⟩⟩
id ┴
src └────┘ └───┘
typ └────┘┴└───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ └┘└─┘
st ─────────────┘└┘
726
727 end second_countable
728
729 section diam
730
731 /-- The diameter of a set in an emetric space, named `emetric.diam` -/
732 def diam (s : set α) := ⨆ (x ∈ s) (y ∈ s), edist x y
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src └─┘ ┴ ┴ └───┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
doc ┴ ┴
733
734 lemma diam_le_iff_forall_edist_le {d : ennreal} :
id └─────┘
src └─────┘
typ └─────┘
doc └─────┘
735 diam s ≤ d ↔ ∀ (x ∈ s) (y ∈ s), edist x y ≤ d :=
id └──┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ └───┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
doc └──┘
736 by simp only [diam, supr_le_iff]
id └──┘ └─────────┘
src └─────────┘└──┘└┘└─────────┘└─
typ └─────────┘└──┘└┘└─────────┘└─
doc └─────────┘└──┘└┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └──────────────────────────────
737
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
738 /-- If two points belong to some set, their edistance is bounded by the diameter of the set -/
739 lemma edist_le_diam_of_mem (hx : x ∈ s) (hy : y ∈ s) : edist x y ≤ diam s :=
id ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └──┘ ┴
src ┴ ┴ └───┘ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └──┘ ┴
doc └──┘
740 diam_le_iff_forall_edist_le.1 (le_refl _) x hx y hy
id └─────────────────────────┘┴ └─────┘ ┴ └┘ ┴ └┘
src └─────────────────────────┘┴ └─────┘
typ └─────────────────────────┘┴ └─────┘ ┴ └┘ ┴ └┘
741
742 /-- If the distance between any two points in a set is bounded by some constant, this constant
743 bounds the diameter. -/
744 lemma diam_le_of_forall_edist_le {d : ennreal} (h : ∀ (x ∈ s) (y ∈ s), edist x y ≤ d) :
id └─────┘ ┴┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src └─────┘ └───┘ ┴
typ └─────┘ ┴┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
doc └─────┘
745 diam s ≤ d :=
id └──┘ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴
doc └──┘
746 diam_le_iff_forall_edist_le.2 h
id └─────────────────────────┘┴ ┴
src └─────────────────────────┘┴
typ └─────────────────────────┘┴ ┴
747
748 /-- The diameter of a subsingleton vanishes. -/
749 lemma diam_subsingleton (hs : s.subsingleton) : diam s = 0 :=
id ┴└───────────┘ └──┘ ┴ ┴
src └───────────┘ └──┘ ┴
typ ┴└───────────┘ └──┘ ┴ ┴
doc └───────────┘ └──┘
750 le_zero_iff_eq.1 $ diam_le_of_forall_edist_le $
id └────────────┘┴ └────────────────────────┘
src └────────────┘┴ └────────────────────────┘
typ └────────────┘┴ └────────────────────────┘
doc └────────────────────────┘
751 λ x hx y hy, (hs hx hy).symm ▸ edist_self y ▸ le_refl _
id ┴ └┘ ┴ └┘ └┘ └┘ └┘ └──┘ ┴ └────────┘ ┴ ┴ └─────┘
src └──┘ ┴ └────────┘ ┴ └─────┘
typ ┴ └┘ ┴ └┘ └┘ └┘ └┘ └──┘ ┴ └────────┘ ┴ ┴ └─────┘
752
753 /-- The diameter of the empty set vanishes -/
754 @[simp] lemma diam_empty : diam (∅ : set α) = 0 :=
id └──┘ ┴ └─┘ ┴ ┴
src └──┘ ┴ └─┘ ┴
typ └──┘ ┴ └─┘ ┴ ┴
doc └──┘ └──┘
755 diam_subsingleton subsingleton_empty
id └───────────────┘ └────────────────┘
src └───────────────┘ └────────────────┘
typ └───────────────┘ └────────────────┘
doc └───────────────┘
756
757 /-- The diameter of a singleton vanishes -/
758 @[simp] lemma diam_singleton : diam ({x} : set α) = 0 :=
id └──┘ ┴┴ └─┘ ┴ ┴
src └──┘ ┴ └─┘ ┴
typ └──┘ ┴┴ └─┘ ┴ ┴
doc └──┘ └──┘
759 diam_subsingleton subsingleton_singleton
id └───────────────┘ └────────────────────┘
src └───────────────┘ └────────────────────┘
typ └───────────────┘ └────────────────────┘
doc └───────────────┘
760
761 lemma diam_eq_zero_iff : diam s = 0 ↔ s.subsingleton :=
id └──┘ ┴ ┴ ┴ ┴└───────────┘
src └──┘ ┴ ┴ └───────────┘
typ └──┘ ┴ ┴ ┴ ┴└───────────┘
doc └──┘ └───────────┘
762 ⟨λ h x hx y hy, edist_le_zero.1 $ h ▸ edist_le_diam_of_mem hx hy, diam_subsingleton⟩
id ┴ ┴ └┘ ┴ └┘ └───────────┘┴ ┴ ┴ └──────────────────┘ └┘ └┘ └───────────────┘
src └───────────┘┴ ┴ └──────────────────┘ └───────────────┘
typ ┴ ┴ └┘ ┴ └┘ └───────────┘┴ ┴ ┴ └──────────────────┘ └┘ └┘ └───────────────┘
doc └──────────────────┘ └───────────────┘
763
764 lemma diam_pos_iff : 0 < diam s ↔ ∃ (x ∈ s) (y ∈ s), x ≠ y :=
id ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴ ┴ ┴
typ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
765 begin
st └─────
766 have := not_congr (@diam_eq_zero_iff _ _ s),
id └───────┘ └──────────────┘ ┴
src └──────┘└───────┘┴ └──────────────┘└───┘ ┴
typ └──────┘└───────┘┴ └──────────────┘└───┘┴┴
doc └──────┘ ┴ └───┘ ┴
txt └──────┘ ┴ └───┘ ┴
par └──────┘ ┴ └───┘ ┴
pid └───┘└─┘ ┴ └───┘ ┴
st ────────────────────────────────────────────┘└─
767 dunfold set.subsingleton at this,
src └──────────────────────────────┘
typ └──────────────────────────────┘
doc └──────────────────────────────┘
txt └──────────────────────────────┘
par └──────────────────────────────┘
pid └───────────────┘└──────┘
st ─────────────────────────────────┘└─
768 push_neg at this,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └──────┘
st ─────────────────┘└─
769 simpa only [zero_lt_iff_ne_zero, exists_prop] using this
id └─────────────────┘ └─────────┘ └──┘
src └──────────┘└─────────────────┘└┘└─────────┘└──────┘ ┴
typ └──────────┘└─────────────────┘└┘└─────────┘└──────┘└──┘┴
doc └──────────┘ └┘ └──────┘ ┴
txt └──────────┘ └┘ └──────┘ ┴
par └──────────┘ └┘ └──────┘ ┴
pid ┴└──┘└┘ └┘ ┴┴└────┘ ┴
st ──────────────────────────────────────────────────────────┘
770 end
st └─┘
771
772 lemma diam_insert : diam (insert x s) = max (diam s) (⨆ y ∈ s, edist y x) :=
id └──┘ └────┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ ┴ ┴┴ └───┘ ┴ ┴
src └──┘ └────┘ ┴ └─┘ └──┘ ┴ ┴ └───┘
typ └──┘ └────┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ ┴ ┴┴ └───┘ ┴ ┴
doc └──┘ └──┘ ┴ ┴
773 eq_of_forall_ge_iff $ λ d, by simp only [diam_le_iff_forall_edist_le, ball_insert_iff, max_le_iff,
id └─────────────────┘ ┴ └─────────────────────────┘ └─────────────┘ └────────┘
src └─────────────────┘ └─────────┘└─────────────────────────┘└┘└─────────────┘└┘└────────┘└─
typ └─────────────────┘ ┴ └─────────┘└─────────────────────────┘└┘└─────────────┘└┘└────────┘└─
doc └─────────┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └─
st └─────────────────────────────────────────────────────────────────────
774 edist_self, zero_le, true_and, supr_le_iff, forall_and_distrib, edist_comm x, and_self,
id └────────┘ └─────┘ └──────┘ └─────────┘ └────────────────┘ └────────┘ ┴ └──────┘
src ─┘└────────┘└┘└─────┘└┘└──────┘└┘└─────────┘└┘└────────────────┘└┘└────────┘┴ └┘└──────┘└─
typ ─┘└────────┘└┘└─────┘└┘└──────┘└┘└─────────┘└┘└────────────────┘└┘└────────┘┴┴└┘└──────┘└─
doc ─┘ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └─
txt ─┘ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └─
par ─┘ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └─
pid ─┘ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └─
st ──────────────────────────────────────────────────────────────────────────────────────────
775 (and_assoc _ _).symm, max_comm (diam s)]
id └───────┘ └──────┘ └──┘ ┴
src ─┘ └───────┘└──────────┘└──────┘┴ └──┘┴ └──
typ ─┘ └───────┘└──────────┘└──────┘┴ └──┘┴┴└──
doc ─┘ └──────────┘ ┴ └──┘┴ └──
txt ─┘ └──────────┘ ┴ ┴ └──
par ─┘ └──────────┘ ┴ ┴ └──
pid ─┘ └──────────┘ ┴ ┴ └┘└
st ───────────────────────────────────────────
776
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
777 lemma diam_pair : diam ({x, y} : set α) = edist x y :=
id └──┘ ┴┴┴ ┴ └─┘ ┴ ┴ └───┘ ┴ ┴
src └──┘ ┴ ┴ └─┘ ┴ └───┘
typ └──┘ ┴┴┴ ┴ └─┘ ┴ ┴ └───┘ ┴ ┴
doc └──┘
778 by simp only [set.insert_of_has_insert, supr_singleton, diam_insert, diam_singleton,
id └──────────────────────┘ └────────────┘ └─────────┘ └────────────┘
src └─────────┘└──────────────────────┘└┘└────────────┘└┘└─────────┘└┘└────────────┘└─
typ └─────────┘└──────────────────────┘└┘└────────────┘└┘└─────────┘└┘└────────────┘└─
doc └─────────┘ └┘ └┘ └┘└────────────┘└─
txt └─────────┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └─
st └──────────────────────────────────────────────────────────────────────────────────
779 ennreal.max_zero_left]
id └───────────────────┘
src ─┘└───────────────────┘└─
typ ─┘└───────────────────┘└─
doc ─┘ └─
txt ─┘ └─
par ─┘ └─
pid ─┘ ┴└
st ─────────────────────────
780
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
781 lemma diam_triple :
782 diam ({x, y, z} : set α) = max (edist x y) (max (edist y z) (edist x z)) :=
id └──┘ ┴┴┴ ┴┴ ┴ └─┘ ┴ ┴ └─┘ └───┘ ┴ ┴ └─┘ └───┘ ┴ ┴ └───┘ ┴ ┴
src └──┘ ┴ ┴ ┴ └─┘ ┴ └─┘ └───┘ └─┘ └───┘ └───┘
typ └──┘ ┴┴┴ ┴┴ ┴ └─┘ ┴ ┴ └─┘ └───┘ ┴ ┴ └─┘ └───┘ ┴ ┴ └───┘ ┴ ┴
doc └──┘
783 by simp only [set.insert_of_has_insert, diam_insert, supr_insert, supr_singleton, diam_singleton,
id └──────────────────────┘ └─────────┘ └─────────┘ └────────────┘ └────────────┘
src └─────────┘└──────────────────────┘└┘└─────────┘└┘└─────────┘└┘└────────────┘└┘└────────────┘└─
typ └─────────┘└──────────────────────┘└┘└─────────┘└┘└─────────┘└┘└────────────┘└┘└────────────┘└─
doc └─────────┘ └┘ └┘ └┘ └┘└────────────┘└─
txt └─────────┘ └┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └─
st └───────────────────────────────────────────────────────────────────────────────────────────────
784 ennreal.max_zero_left, ennreal.sup_eq_max]
id └───────────────────┘ └────────────────┘
src ─┘└───────────────────┘└┘└────────────────┘└─
typ ─┘└───────────────────┘└┘└────────────────┘└─
doc ─┘ └┘ └─
txt ─┘ └┘ └─
par ─┘ └┘ └─
pid ─┘ └┘ ┴└
st ─────────────────────────────────────────────
785
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
786 /-- The diameter is monotonous with respect to inclusion -/
787 lemma diam_mono {s t : set α} (h : s ⊆ t) : diam s ≤ diam t :=
id └─┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src └─┘ ┴ └──┘ ┴ └──┘
typ └─┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └──┘ └──┘
788 diam_le_of_forall_edist_le $ λ x hx y hy, edist_le_diam_of_mem (h hx) (h hy)
id └────────────────────────┘ ┴ └┘ ┴ └┘ └──────────────────┘ ┴ └┘ ┴ └┘
src └────────────────────────┘ └──────────────────┘
typ └────────────────────────┘ ┴ └┘ ┴ └┘ └──────────────────┘ ┴ └┘ ┴ └┘
doc └────────────────────────┘ └──────────────────┘
789
790 /-- The diameter of a union is controlled by the diameter of the sets, and the edistance
791 between two points in the sets. -/
792 lemma diam_union {t : set α} (xs : x ∈ s) (yt : y ∈ t) : diam (s ∪ t) ≤ diam s + edist x y + diam t :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ └──┘ ┴
src └─┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ └───┘ ┴ └──┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ └──┘ ┴
doc └──┘ └──┘ └──┘
793 begin
st └─────
794 have A : ∀a ∈ s, ∀b ∈ t, edist a b ≤ diam s + edist x y + diam t := λa ha b hb, calc
id ┴ ┴ ┴ └───┘ ┴ ┴ └──┘ ┴
src └───────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴└───┘┴ ┴ ┴ ┴└──┘┴ └──┘ └─────────┘ └
typ └───────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴┴┴ ┴┴┴┴┴└───┘┴┴┴┴┴ ┴└──┘┴┴└──┘ └─────────┘ └
doc └───────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘┴ └──┘ └─────────┘ └
txt └───────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─────────┘ └
par └───────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─────────┘ └
pid └────┘└─┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─────────┘ └
st ───────────────────────────────────────────────────────────────────────────────────────
795 edist a b ≤ edist a x + edist x y + edist y b : edist_triangle4 _ _ _ _
id └─────────────┘
src ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└─────────────┘└────────
typ ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└─────────────┘└────────
doc ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────────
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────────
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────────
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────────
st ────────────────────────────────────────────────────────────────────────────
796 ... ≤ diam s + edist x y + diam t :
id ┴ └───┘ ┴ ┴ └──┘ ┴
src ───────┘ ┴ ┴ ┴ ┴└───┘┴ ┴ ┴ ┴└──┘┴ └──
typ ───────┘ ┴ ┴┴┴ ┴└───┘┴┴┴┴┴ ┴└──┘┴┴└──
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘┴ └──
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
st ────────────────────────────────────────
797 add_le_add' (add_le_add' (edist_le_diam_of_mem ha xs) (le_refl _)) (edist_le_diam_of_mem yt hb),
id └─────────┘ └┘ └─────┘ └──────────────────┘ └┘
src ─────┘ ┴ └─────────┘┴ ┴ ┴ └┘ └─────┘└───┘ └──────────────────┘┴ ┴ ┴
typ ─────┘ ┴ └─────────┘┴ ┴ ┴└┘└┘ └─────┘└───┘ └──────────────────┘┴└┘┴ ┴
doc ─────┘ ┴ ┴ ┴ ┴ └┘ └───┘ └──────────────────┘┴ ┴ ┴
txt ─────┘ ┴ ┴ ┴ ┴ └┘ └───┘ ┴ ┴ ┴
par ─────┘ ┴ ┴ ┴ ┴ └┘ └───┘ ┴ ┴ ┴
pid ─────┘ ┴ ┴ ┴ ┴ └┘ └───┘ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
798 refine diam_le_of_forall_edist_le (λa ha b hb, _),
id └────────────────────────┘
src └─────┘└────────────────────────┘┴ └───────────┘
typ └─────┘└────────────────────────┘┴ └───────────┘
doc └─────┘└────────────────────────┘┴ └───────────┘
txt └─────┘ ┴ └───────────┘
par └─────┘ ┴ └───────────┘
pid ┴ ┴ └───────────┘
st ──────────────────────────────────────────────────┘└─
799 cases (mem_union _ _ _).1 ha with h'a h'a; cases (mem_union _ _ _).1 hb with h'b h'b,
id └───────┘ └┘ └───────┘ └┘
src └────┘ └───────┘└────────┘ └───────────┘ └────┘ └───────┘└────────┘ └───────────┘
typ └────┘ └───────┘└────────┘└┘└───────────┘ └────┘ └───────┘└────────┘└┘└───────────┘
doc └────┘ └────────┘ └───────────┘ └────┘ └────────┘ └───────────┘
txt └────┘ └────────┘ └───────────┘ └────┘ └────────┘ └───────────┘
par └────┘ └────────┘ └───────────┘ └────┘ └────────┘ └───────────┘
pid ┴ └────────┘ └───────────┘ ┴ └────────┘ └───────────┘
st ─────────────────────────────────────────────────────────────────────────────────────┘└─
800 { calc edist a b ≤ diam s : edist_le_diam_of_mem h'a h'b
id └──┘ ┴ ┴ └──┘ ┴ └──────────────────┘ └─┘ └─┘
src └──┘ └──┘ └──────────────────┘
typ └──┘ ┴ ┴ └──┘ ┴ └──────────────────┘ └─┘ └─┘
doc └──┘ └──┘ └──────────────────┘
st ───┘└──────────────────────────────────────────────────────
801 ... ≤ diam s + (edist x y + diam t) : le_add_right (le_refl _)
id └──────────┘ └─────┘
src └──────────┘ └─────┘
typ └──────────┘ └─────┘
st ───────────────────────────────────────────────────────────────────────
802 ... = diam s + edist x y + diam t : by simp only [add_comm, eq_self_iff_true, add_left_comm] },
id └───┘ ┴ ┴ ┴ └──────┘ └──────────────┘ └───────────┘
src └───┘ └─────────┘└──────┘└┘└──────────────┘└┘└───────────┘└┘
typ └───┘ ┴ ┴ ┴ └─────────┘└──────┘└┘└──────────────┘└┘└───────────┘└┘
doc └─────────┘ └┘ └┘ └┘
txt └─────────┘ └┘ └┘ └┘
par └─────────┘ └┘ └┘ └┘
pid ┴└──┘└┘ └┘ └┘ ┴┴
st ─────────────────────────────────────────────┘└─────────────────────────────────────────────────────┘└┘└
803 { exact A a h'a b h'b },
id ┴ ┴ └─┘ ┴ └─┘
src └────┘ ┴ ┴ ┴ ┴ ┴
typ └────┘┴┴┴┴└─┘┴┴┴└─┘┴
doc └────┘ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ───┘└──────────────────┘└┘└
804 { have Z := A b h'b a h'a, rwa [edist_comm] at Z },
id ┴ ┴ └─┘ ┴ └─┘ └────────┘
src └────────┘ ┴ ┴ ┴ ┴ └───┘└────────┘└─────┘
typ └────────┘┴┴┴┴└─┘┴┴┴└─┘ └───┘└────────┘└─────┘
doc └────────┘ ┴ ┴ ┴ ┴ └───┘ └─────┘
txt └────────┘ ┴ ┴ ┴ ┴ └───┘ └─────┘
par └────────┘ ┴ ┴ ┴ ┴ └───┘ └─────┘
pid └────┘┴└─┘ ┴ ┴ ┴ ┴ └┘ ┴└───┘┴
st ───┘└─────────────────────┘└───────────────┘┴└────┘└┘└
805 { calc edist a b ≤ diam t : edist_le_diam_of_mem h'a h'b
id └──┘ ┴ ┴ └──────────────────┘ └─┘ └─┘
src └──┘ └──────────────────┘
typ └──┘ ┴ ┴ └──────────────────┘ └─┘ └─┘
doc └──┘ └──────────────────┘
st ───────────────────────────────────────────────────────────
806 ... ≤ (diam s + edist x y) + diam t : le_add_left (le_refl _) }
id ┴ └───┘ ┴ ┴ └──┘ ┴ └─────────┘ └─────┘
src └───┘ └──┘ └─────────┘ └─────┘
typ ┴ └───┘ ┴ ┴ └──┘ ┴ └─────────┘ └─────┘
doc └──┘
st ────────────────────────────────────────────────────────────────────┘└──
807 end
st ──┘
808
809 lemma diam_union' {t : set α} (h : (s ∩ t).nonempty) : diam (s ∪ t) ≤ diam s + diam t :=
id └─┘ ┴ ┴ ┴ ┴ └──────┘ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src └─┘ ┴ └──────┘ └──┘ ┴ ┴ └──┘ ┴ └──┘
typ └─┘ ┴ ┴ ┴ ┴ └──────┘ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └──────┘ └──┘ └──┘ └──┘
810 let ⟨x, ⟨xs, xt⟩⟩ := h in by simpa using diam_union xs xt
id └─┘ ┴ └────────┘ └┘ └┘
src └──────────┘└────────┘┴ ┴ └
typ └─┘ ┴ └──────────┘└────────┘┴└┘┴└┘└
doc └──────────┘└────────┘┴ ┴ └
txt └──────────┘ ┴ ┴ └
par └──────────┘ ┴ ┴ └
pid ┴└────┘ ┴ ┴ └
st └─────────────────────────────
811
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
812 lemma diam_closed_ball {r : ennreal} : diam (closed_ball x r) ≤ 2 * r :=
id └─────┘ └──┘ └─────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──┘ └─────────┘ ┴ ┴
typ └─────┘ └──┘ └─────────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └──┘ └─────────┘
813 diam_le_of_forall_edist_le $ λa ha b hb, calc
id └────────────────────────┘ ┴ └┘ ┴ └┘
src └────────────────────────┘
typ └────────────────────────┘ ┴ └┘ ┴ └┘
doc └────────────────────────┘
814 edist a b ≤ edist a x + edist b x : edist_triangle_right _ _ _
id └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └──────────────────┘
src └───┘ └───┘ ┴ └───┘ └──────────────────┘
typ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └──────────────────┘
815 ... ≤ r + r : add_le_add' ha hb
id ┴ ┴ ┴ └─────────┘ └┘ └┘
src ┴ └─────────┘
typ ┴ ┴ ┴ └─────────┘ └┘ └┘
816 ... = 2 * r : by simp [mul_two, mul_comm]
id ┴ ┴ └─────┘ └──────┘
src ┴ └────┘└─────┘└┘└──────┘└─
typ ┴ ┴ └────┘└─────┘└┘└──────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └─────────────────────────
817
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
818 lemma diam_ball {r : ennreal} : diam (ball x r) ≤ 2 * r :=
id └─────┘ └──┘ └──┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──┘ └──┘ ┴ ┴
typ └─────┘ └──┘ └──┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └──┘ └──┘
819 le_trans (diam_mono ball_subset_closed_ball) diam_closed_ball
id └──────┘ └───────┘ └─────────────────────┘ └──────────────┘
src └──────┘ └───────┘ └─────────────────────┘ └──────────────┘
typ └──────┘ └───────┘ └─────────────────────┘ └──────────────┘
doc └───────┘
820
821 end diam
822
823 end emetric --namespace